Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/z3_09_09_8h_source.html below:

Z3: src/api/c++/z3++.h Source File

*

()

{

m_msg.c_str(); }

*

()

throw() {

m_msg.c_str(); }

Z3_config()

{

m_cfg; }

(

* param,

value) {

str = std::to_string(value);

m_enable_exceptions =

;

m_enable_exceptions =

;

m_rounding_mode =

;

detach() { m_ctx =

; }

(

* param,

value) {

str = std::to_string(value);

<

precision>

(

* name,

ebits,

sbits);

<

precision>

<

T>

std::unique_ptr<T[]> m_array;

(

sz):m_array(new T[sz]),m_size(sz) {}

<

T2>

(

sz) { m_array.reset(

T[sz]); m_size = sz; }

()

{

m_size; }

T &

(

i) { assert(0 <= i); assert(

(i) < m_size);

m_array[i]; }

T

&

(

i)

{ assert(0 <= i); assert(

(i) < m_size);

m_array[i]; }

T

*

()

{

m_array.get(); }

T *

() {

m_array.get(); }

(

& a,

& b);

out <<

<< s.

();

Z3_param_descrs m_descrs;

m_descrs = o.m_descrs;

object::operator=(o);

object::operator=(s);

m_params = s.m_params;

bool()

{

!= 0; }

object::operator=(s);

std::ostream &

(std::ostream & out,

& n);

(

& a,

& b);

<

T>

object::operator=(s);

m_vector = s.m_vector;

other.m_index == m_index;

other.m_index != m_index;

expr

(expr

& a, expr

& i);

assert(

().enable_exceptions());

(!

().enable_exceptions())

0;

result = 0;

assert(

().enable_exceptions());

(!

().enable_exceptions())

0;

assert(

().enable_exceptions());

(!

().enable_exceptions())

0;

uint64_t result = 0;

assert(

().enable_exceptions());

(!

().enable_exceptions())

0;

std::string(s);

(

i = 0; i < argCnt; i++)

(*

, index);

(*

, index);

i == other.i;

i != other.i;

args[2] = { a, b };

args[2] = { a, b };

args[2] = { a, b };

args[2] = { a, b };

_args[2] = { a, b };

args[2] = { a, b };

(a.

()) {

args[2] = { a, b };

(a.

()) {

(a.

()) {

assert(a.

());

assert(a.

());

ge = a >= zero;

ge = a >= zero;

assert(t.

());

assert(t.

());

<

T>

<

T2>

(

i = 0; i < m_size; i++) {

assert(es.

() > 0);

(ctx, r);

assert(es.

() > 0);

(ctx, r);

assert(es.

() > 0);

(ctx, r);

assert(es.

() > 0);

(ctx, r);

assert(es.

() > 0);

(ctx, r);

assert(args.

() > 0);

(ctx, r);

assert(args.

() > 0);

(ctx, r);

_args[2] = { a, b };

_args[2] = { a, b };

assert(args.

() > 0);

(args.

() == 1) {

r = _args[args.

()-1];

(

i = args.

()-1; i > 0; ) {

(ctx, r);

(ctx, r);

(ctx, r);

(ctx, r);

(ctx, r);

(args.

(), r);

(args.

(), r);

(

i = 1; i < args.

(); ++i)

object::operator=(s);

m_entry = s.m_entry;

object::operator=(s);

m_interp = s.m_interp;

object::operator=(s);

m_model = s.m_model;

(status ==

&&

().enable_exceptions())

std::ostream &

(std::ostream & out,

& m);

object::operator=(s);

m_stats = s.m_stats;

std::ostream &

(std::ostream & out,

& s);

(r ==

) out <<

;

(r ==

) out <<

;

out <<

;

& ctx()

{

m_decl.

(); }

check_error()

{ ctx().

(); }

(ctx().enable_exceptions() && idx >= m_decl.

())

object::operator=(s);

m_solver = s.m_solver;

(e,

().bool_const(p));

(

i = 0; i < v.

(); ++i)

(

i = 0; i < n; i++) {

_assumptions[i] = assumptions[i];

n = assumptions.

();

(

i = 0; i < n; i++) {

_assumptions[i] = assumptions[i];

sz = result.

();

std::string

(

* status =

) {

sz = es.

();

,

, status,

,

& m_cutoff;

assert(!m_end && !m_empty);

m_cube = m_solver.

(m_vars, m_cutoff);

m_cutoff = 0xFFFFFFFF;

(m_cube.

() == 1 && m_cube[0u].is_false()) {

(m_cube.

()) {

other.m_end == m_end;

other.m_end != m_end;

m_cutoff(0xFFFFFFFF),

m_default_vars(s.

()),

m_vars(m_default_vars)

m_cutoff(0xFFFFFFFF),

m_default_vars(s.

()),

init(Z3_goal s) {

(

& c,

models=

,

unsat_cores=

,

proofs=

):

(c) { init(

(c, models, unsat_cores, proofs)); }

Z3_goal()

{

m_goal; }

object::operator=(s);

n =

();

(

i = 0; i < n; i++)

args[i] =

[](i);

std::ostream &

(std::ostream & out,

& g);

Z3_apply_result m_apply_result;

init(Z3_apply_result s) {

Z3_apply_result()

{

m_apply_result; }

object::operator=(s);

m_apply_result = s.m_apply_result;

init(Z3_tactic s) {

Z3_tactic()

{

m_tactic; }

object::operator=(s);

m_tactic = s.m_tactic;

(

(

));

(

i = 0; i < n; ++i) buffer[i] =

[i];

Z3_simplifier m_simplifier;

init(Z3_simplifier s) {

Z3_simplifier()

{

m_simplifier; }

object::operator=(s);

m_simplifier = s.m_simplifier;

init(Z3_probe s) {

Z3_probe()

{

m_probe; }

object::operator=(s);

m_probe = s.m_probe;

()

{

m_h; }

(expr_vector::iterator it = v.

(); it != v.

(); ++it)

(*it);

object::operator=(o);

Z3_optimize()

{

m_opt; }

(expr_vector::iterator it = es.

(); it != es.

(); ++it)

(*it);

(e,

().bool_const(p));

str = std::to_string(weight);

n = asms.

();

(

i = 0; i < n; i++) {

object::operator=(o);

Z3_fixedpoint()

{

m_fp; }

(

i = 0; i < n; i++) { _enum_names[i] =

(*

, enum_names[i]); }

(

i = 0; i < n; i++) { _names[i] =

(*

, names[i]); _sorts[i] = sorts[i]; }

(

i = 0; i < n; i++) { projs.

(

(*

, _projs[i])); }

Z3_constructor_list clist;

Z3_constructor_list()

{

clist; }

std::vector<Z3_constructor> cons;

std::vector<unsigned> num_fields;

(

con : cons)

(

i = 0; i < n; ++i) sorts[i] = fields[i], _names[i] = names[i];

num_fields.push_back(n);

Z3_constructor

(

i)

{

cons[i]; }

()

{

(

)cons.size(); }

constructor =

(ctx, _constructor);

(

j = 0; j < num_fields[i]; ++j)

(

i = 0; i < cs.

(); ++i)

(

i = 0; i < cs.

(); ++i) _cs[i] = cs[i];

(*

, s);

n,

* names,

(

i = 0; i < n; ++i)

_names[i] = names[i], _cons[i] = *cons[i];

(

i = 0; i < n; ++i)

(*

, s);

(

i = 0; i < arity; i++) {

args[i] = domain[i];

(

i = 0; i < domain.

(); i++) {

args[i] = domain[i];

args[3] = { d1, d2, d3 };

args[4] = { d1, d2, d3, d4 };

args[5] = { d1, d2, d3, d4, d5 };

(

i = 0; i < arity; i++) {

args[i] = domain[i];

dom[2] = { d1, d2 };

(*

, r);

(*

, r);

<

precision>

(m_rounding_mode) {

:

(*

);

(

i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;

(

i = 0; i < n; i++) {

(

i = 0; i < args.

(); i++) {

args[2] = { a1, a2 };

args[3] = { a1, a2, a3 };

args[4] = { a1, a2, a3, a4 };

args[5] = { a1, a2, a3, a4, a5 };

assert(args.

() > 0);

(ctx, r);

(ctx, r);

(

i = 0; i < sorts.

(); ++i) {

sort_names[i] = sorts[i].name();

(

i = 0; i < decls.

(); ++i) {

decl_names[i] = decls[i].name();

(

i = 0; i < sorts.

(); ++i) {

sort_names[i] = sorts[i].name();

(

i = 0; i < decls.

(); ++i) {

decl_names[i] = decls[i].name();

(

i = 0; i < n; ++i)

(

i = 0; i < n; ++i)

(; idx < n; ++idx) {

(

() == f.

())

(

i = 0; i < n; ++i)

assert(src.

() == dst.

());

(

i = 0; i < src.

(); ++i) {

(

i = 0; i < dst.

(); ++i) {

(dst.

() != funs.

()) {

(

(),

);

(

i = 0; i < dst.

(); ++i) {

_on_clause_eh(

* _ctx,

_proof,

n,

* dep,

_literals) {

proof(ctx->c, _proof);

std::vector<unsigned> deps;

(

i = 0; i < n; ++i)

deps.push_back(dep[i]);

ctx->m_on_clause(proof, deps, lits);

final_eh_t m_final_eh;

fixed_eh_t m_fixed_eh;

created_eh_t m_created_eh;

decide_eh_t m_decide_eh;

std::vector<z3::context*> subcontexts;

scoped_cb _cb(p, cb);

scoped_cb _cb(p, cb);

p->subcontexts.push_back(c);

p->

(*c);

scoped_cb _cb(p, cb);

value(p->

(), _value);

p->m_fixed_eh(var, value);

scoped_cb _cb(p, cb);

scoped_cb _cb(p, cb);

scoped_cb _cb(p, cb);

scoped_cb _cb(p, cb);

p->m_decide_eh(val, bit, is_pos);

(

num_scopes) = 0;

(

& subcontext : subcontexts) {

subcontext->detach();

c ? *c : s->

();

m_fixed_eh = [

](

&id,

&e) {

m_eq_eh = [

](

& x,

& y) {

m_final_eh = [

]() {

m_created_eh = [

](

& e) {

m_decide_eh = [

](

val,

bit,

is_pos) {

(val, bit, is_pos);

() { }

assert(lhs.

() == rhs.

());

& conseq) {

assert(lhs.

() == rhs.

());

apply_result & operator=(apply_result const &s)

apply_result(context &c, Z3_apply_result s)

goal operator[](int i) const

apply_result(apply_result const &s)

friend std::ostream & operator<<(std::ostream &out, apply_result const &r)

T const & operator[](int i) const

iterator(ast_vector_tpl const *v, unsigned i)

bool operator==(iterator const &other) const noexcept

iterator operator++(int) noexcept

iterator & operator++() noexcept

bool operator!=(iterator const &other) const noexcept

friend std::ostream & operator<<(std::ostream &out, ast_vector_tpl const &v)

ast_vector_tpl & set(unsigned idx, ast &a)

~ast_vector_tpl() override

ast_vector_tpl(ast_vector_tpl const &s)

ast_vector_tpl(context &c, Z3_ast_vector v)

void push_back(T const &e)

std::string to_string() const

ast_vector_tpl & operator=(ast_vector_tpl const &s)

T operator[](unsigned i) const

ast_vector_tpl(context &c, ast_vector_tpl const &src)

ast_vector_tpl(context &c)

iterator begin() const noexcept

ast & operator=(ast const &s)

friend bool eq(ast const &a, ast const &b)

Return true if the ASTs are structurally identical.

std::string to_string() const

ast(context &c, Z3_ast n)

friend std::ostream & operator<<(std::ostream &out, ast const &n)

ast operator()(context &c, Z3_ast a)

expr operator()(context &c, Z3_ast a)

func_decl operator()(context &c, Z3_ast a)

sort operator()(context &c, Z3_ast a)

Z3 global configuration object.

void set(char const *param, int value)

Set global parameter param with integer value.

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

Set global parameter param with string value.

void set(char const *param, bool value)

Set global parameter param with Boolean value.

constructor_list(constructors const &cs)

void query(unsigned i, func_decl &constructor, func_decl &test, func_decl_vector &accs)

constructors(context &ctx)

Z3_constructor operator[](unsigned i) const

void add(symbol const &name, symbol const &rec, unsigned n, symbol const *names, sort const *fields)

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

symbol str_symbol(char const *s)

Create a Z3 symbol based on the given string.

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.

expr num_val(int n, sort const &s)

expr bv_val(int n, unsigned sz)

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

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

expr string_val(char const *s)

sort real_sort()

Return the Real sort.

Z3_error_code check_error() const

Auxiliary method used to check for API usage errors.

expr bv_const(char const *name, unsigned sz)

expr string_const(char const *name)

sort array_sort(sort d, sort r)

Return an array sort for arrays from d to r.

void set_enable_exceptions(bool f)

The C++ API uses by defaults exceptions on errors. For applications that don't work well with excepti...

sort string_sort()

Return the sort for Unicode strings.

sort re_sort(sort &seq_sort)

Return a regular expression sort over sequences seq_sort.

sort uninterpreted_sort(char const *name)

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

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

void set(char const *param, int value)

Update global parameter param with Integer value.

sort bool_sort()

Return the Boolean sort.

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

Update global parameter param with string value.

expr bool_const(char const *name)

create uninterpreted constants of a given sort.

void check_parser_error() const

expr variable(unsigned index, sort const &s)

create a de-Bruijn variable.

expr_vector parse_string(char const *s)

parsing

symbol int_symbol(int n)

Create a Z3 symbol based on the given integer.

expr real_const(char const *name)

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 nu...

expr int_const(char const *name)

expr fpa_nan(sort const &s)

bool enable_exceptions() const

sort bv_sort(unsigned sz)

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

expr fpa_inf(sort const &s, bool sgn)

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

sort fpa_rounding_mode_sort()

Return a RoundingMode sort.

expr_vector parse_file(char const *file)

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

create an uninterpreted constant.

sort char_sort()

Return the sort for Unicode characters.

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 argumen...

void set(char const *param, bool value)

Update global parameter param with Boolean value.

sort int_sort()

Return the integer sort.

void interrupt()

Interrupt the current procedure being executed by any object managed by this context....

void set_rounding_mode(rounding_mode rm)

Sets RoundingMode of FloatingPoints.

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

sort fpa_sort()

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

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 name...

sort datatype_sort(symbol const &name)

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

sort seq_sort(sort &s)

Return a sequence sort over base sort s.

Exception used to sign API usage errors.

friend std::ostream & operator<<(std::ostream &out, exception const &e)

virtual ~exception()=default

char const * what() const

bool operator==(iterator const &other) const noexcept

iterator(expr &e, unsigned i)

bool operator!=(iterator const &other) const noexcept

A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort ...

bool is_lambda() const

Return true if this expression is a lambda expression.

friend expr pw(expr const &a, expr const &b)

friend expr sbv_to_fpa(expr const &t, sort s)

Conversion of a signed bit-vector term into a floating-point.

friend expr bvneg_no_overflow(expr const &a)

expr loop(unsigned lo, unsigned hi)

expr body() const

Return the 'body' of this quantifier.

friend expr bvadd_no_underflow(expr const &a, expr const &b)

friend expr sum(expr_vector const &args)

expr substitute(expr_vector const &src, expr_vector const &dst)

Apply substitution. Replace src expressions by dst.

bool is_quantifier() const

Return true if this expression is a quantifier.

bool is_exists() const

Return true if this expression is an existential quantifier.

bool is_numeral_u64(uint64_t &i) const

bool is_int() const

Return true if this is an integer expression.

friend expr operator/(expr const &a, expr const &b)

friend expr fp_eq(expr const &a, expr const &b)

friend expr concat(expr const &a, expr const &b)

friend expr bvmul_no_underflow(expr const &a, expr const &b)

int64_t get_numeral_int64() const

Return int64_t value of numeral, throw if result cannot fit in int64_t.

bool is_app() const

Return true if this expression is an application.

friend expr fpa_to_fpa(expr const &t, sort s)

Conversion of a floating-point term into another floating-point.

friend expr operator&&(expr const &a, expr const &b)

Return an expression representing a and b.

friend expr operator!=(expr const &a, expr const &b)

friend expr operator+(expr const &a, expr const &b)

std::string get_string() const

for a string value expression return an escaped string value.

bool is_numeral(std::string &s) const

bool is_var() const

Return true if this expression is a variable.

bool is_numeral_u(unsigned &i) const

friend expr min(expr const &a, expr const &b)

expr at(expr const &index) const

expr_vector args() const

Return a vector of all the arguments of this application. This method assumes the expression is an ap...

bool is_real() const

Return true if this is a real expression.

bool is_numeral_i(int &i) const

friend expr operator>(expr const &a, expr const &b)

expr mk_is_nan() const

Return Boolean expression to test for whether an FP expression is a NaN.

int get_numeral_int() const

Return int value of numeral, throw if result cannot fit in machine int.

friend expr bv2int(expr const &a, bool is_signed)

bit-vector and integer conversions.

friend expr operator~(expr const &a)

unsigned num_args() const

Return the number of arguments in this application. This method assumes the expression is an applicat...

friend expr nor(expr const &a, expr const &b)

friend expr fpa_fp(expr const &sgn, expr const &exp, expr const &sig)

Create an expression of FloatingPoint sort from three bit-vector expressions.

expr arg(unsigned i) const

Return the i-th argument of this application. This method assumes the expression is an application.

expr mk_is_normal() const

Return Boolean expression to test for whether an FP expression is a normal.

friend expr bvsub_no_underflow(expr const &a, expr const &b, bool is_signed)

expr repeat(unsigned i) const

friend expr mk_xor(expr_vector const &args)

bool is_numeral(std::string &s, unsigned precision) const

unsigned get_numeral_uint() const

Return uint value of numeral, throw if result cannot fit in machine uint.

bool is_numeral(double &d) const

expr rotate_left(unsigned i) const

friend expr operator*(expr const &a, expr const &b)

sort get_sort() const

Return the sort of this expression.

friend expr nand(expr const &a, expr const &b)

friend expr fpa_to_ubv(expr const &t, unsigned sz)

Conversion of a floating-point term into an unsigned bit-vector.

friend expr bvredor(expr const &a)

expr extract(unsigned hi, unsigned lo) const

expr rotate_right(unsigned i) const

friend expr int2bv(unsigned n, expr const &a)

friend expr max(expr const &a, expr const &b)

bool is_relation() const

Return true if this is a Relation expression.

friend expr xnor(expr const &a, expr const &b)

friend expr abs(expr const &a)

friend expr pbge(expr_vector const &es, int const *coeffs, int bound)

bool is_well_sorted() const

Return true if this expression is well sorted (aka type correct).

friend expr round_fpa_to_closest_integer(expr const &t)

Round a floating-point term into its closest integer.

friend expr distinct(expr_vector const &args)

friend expr bvmul_no_overflow(expr const &a, expr const &b, bool is_signed)

friend expr bvsub_no_overflow(expr const &a, expr const &b)

bool is_const() const

Return true if this expression is a constant (i.e., an application with 0 arguments).

friend expr mod(expr const &a, expr const &b)

friend expr fma(expr const &a, expr const &b, expr const &c, expr const &rm)

FloatingPoint fused multiply-add.

bool is_bool() const

Return true if this is a Boolean expression.

friend expr mk_or(expr_vector const &args)

expr contains(expr const &s) const

friend expr ite(expr const &c, expr const &t, expr const &e)

Create the if-then-else expression ite(c, t, e)

expr algebraic_lower(unsigned precision) const

expr simplify() const

Return a simplified version of this expression.

bool is_arith() const

Return true if this is an integer or real expression.

expr mk_is_inf() const

Return Boolean expression to test for whether an FP expression is inf.

expr_vector algebraic_poly() const

Return coefficients for p of an algebraic number (root-obj p i)

bool is_bv() const

Return true if this is a Bit-vector expression.

friend expr pbeq(expr_vector const &es, int const *coeffs, int bound)

friend expr operator^(expr const &a, expr const &b)

friend expr operator<=(expr const &a, expr const &b)

friend expr operator>=(expr const &a, expr const &b)

friend expr sqrt(expr const &a, expr const &rm)

friend expr pble(expr_vector const &es, int const *coeffs, int bound)

friend expr operator==(expr const &a, expr const &b)

bool is_finite_domain() const

Return true if this is a Finite-domain expression.

expr operator[](expr_vector const &index) const

bool is_forall() const

Return true if this expression is a universal quantifier.

uint64_t as_uint64() const

friend expr implies(expr const &a, expr const &b)

expr mk_is_subnormal() const

Return Boolean expression to test for whether an FP expression is a subnormal.

uint64_t get_numeral_uint64() const

Return uint64_t value of numeral, throw if result cannot fit in uint64_t.

expr(context &c, Z3_ast n)

friend expr bvadd_no_overflow(expr const &a, expr const &b, bool is_signed)

bit-vector overflow/underflow checks

bool is_datatype() const

Return true if this is a Datatype expression.

bool is_string_value() const

Return true if this expression is a string literal. The string can be accessed using get_string() and...

expr simplify(params const &p) const

Return a simplified version of this expression. The parameter p is a set of parameters for the Z3 sim...

expr loop(unsigned lo)

create a looping regular expression.

expr mk_from_ieee_bv(sort const &s) const

Convert this IEEE BV into a fpa.

friend expr bvredand(expr const &a)

friend expr operator&(expr const &a, expr const &b)

friend expr operator-(expr const &a)

friend expr bvsdiv_no_overflow(expr const &a, expr const &b)

expr extract(expr const &offset, expr const &length) const

sequence and regular expression operations.

bool is_re() const

Return true if this is a regular expression.

bool is_numeral_i64(int64_t &i) const

bool as_binary(std::string &s) const

unsigned id() const

retrieve unique identifier for expression.

friend expr rem(expr const &a, expr const &b)

friend expr operator!(expr const &a)

Return an expression representing not(a).

bool is_algebraic() const

Return true if expression is an algebraic number.

friend expr mk_and(expr_vector const &args)

expr mk_is_zero() const

Return Boolean expression to test for whether an FP expression is a zero.

std::u32string get_u32string() const

for a string value expression return an unespaced string value.

std::string get_decimal_string(int precision) const

Return string representation of numeral or algebraic number This method assumes the expression is num...

Z3_lbool bool_value() const

expr replace(expr const &src, expr const &dst) const

friend expr operator||(expr const &a, expr const &b)

Return an expression representing a or b.

bool is_array() const

Return true if this is a Array expression.

unsigned algebraic_i() const

Return i of an algebraic number (root-obj p i)

friend expr ubv_to_fpa(expr const &t, sort s)

Conversion of an unsigned bit-vector term into a floating-point.

expr nth(expr const &index) const

friend expr fpa_to_sbv(expr const &t, unsigned sz)

Conversion of a floating-point term into a signed bit-vector.

bool is_seq() const

Return true if this is a sequence expression.

friend expr operator|(expr const &a, expr const &b)

expr bit2bool(unsigned i) const

friend expr atmost(expr_vector const &es, unsigned bound)

friend expr range(expr const &lo, expr const &hi)

expr char_from_bv() const

friend expr atleast(expr_vector const &es, unsigned bound)

friend expr operator<(expr const &a, expr const &b)

expr mk_to_ieee_bv() const

Convert this fpa into an IEEE BV.

expr operator[](expr const &index) const

expr algebraic_upper(unsigned precision) const

bool is_numeral() const

Return true if this expression is a numeral. Specialized functions also return representations for th...

bool is_fpa() const

Return true if this is a FloatingPoint expression. .

func_decl decl() const

Return the declaration associated with this application. This method assumes the expression is an app...

std::string to_string(expr_vector const &queries)

expr_vector from_string(char const *s)

void add_fact(func_decl &f, unsigned *args)

fixedpoint & operator=(fixedpoint const &o)

void add_cover(int level, func_decl &p, expr &property)

expr_vector rules() const

expr get_cover_delta(int level, func_decl &p)

std::string reason_unknown()

check_result query(func_decl_vector &relations)

void register_relation(func_decl &p)

check_result query(expr &q)

param_descrs get_param_descrs()

expr_vector from_file(char const *s)

void update_rule(expr &rule, symbol const &name)

expr_vector assertions() const

fixedpoint(fixedpoint const &o)

unsigned get_num_levels(func_decl &p)

void add_rule(expr &rule, symbol const &name)

void set(params const &p)

Function declaration (aka function definition). It is the signature of interpreted and uninterpreted ...

func_decl transitive_closure(func_decl const &)

func_decl(context &c, Z3_func_decl n)

func_decl_vector accessors()

Z3_decl_kind decl_kind() const

sort domain(unsigned i) const

unsigned id() const

retrieve unique identifier for func_decl.

unsigned num_parameters() const

func_entry & operator=(func_entry const &s)

unsigned num_args() const

expr arg(unsigned i) const

func_entry(context &c, Z3_func_entry e)

func_entry(func_entry const &s)

void set_else(expr &value)

func_interp(context &c, Z3_func_interp e)

func_interp(func_interp const &s)

func_interp & operator=(func_interp const &s)

func_entry entry(unsigned i) const

void add_entry(expr_vector const &args, expr &value)

unsigned num_entries() const

Z3_goal_prec precision() const

model convert_model(model const &m) const

bool is_decided_unsat() const

friend std::ostream & operator<<(std::ostream &out, goal const &g)

bool inconsistent() const

std::string dimacs(bool include_names=true) const

unsigned num_exprs() const

goal(context &c, Z3_goal s)

goal & operator=(goal const &s)

goal(context &c, bool models=true, bool unsat_cores=false, bool proofs=false)

void add(expr_vector const &v)

bool is_decided_sat() const

expr operator[](int i) const

expr eval(expr const &n, bool model_completion=false) const

expr get_const_interp(func_decl c) const

unsigned num_consts() const

unsigned num_funcs() const

friend std::ostream & operator<<(std::ostream &out, model const &m)

model & operator=(model const &s)

func_interp get_func_interp(func_decl f) const

func_decl get_func_decl(unsigned i) const

func_interp add_func_interp(func_decl &f, expr &else_val)

func_decl operator[](int i) const

void add_const_interp(func_decl &f, expr &value)

func_decl get_const_decl(unsigned i) const

bool has_interp(func_decl f) const

std::string to_string() const

model(model &src, context &dst, translate)

model(context &c, Z3_model m)

Z3_error_code check_error() const

friend void check_context(object const &a, object const &b)

virtual ~object()=default

on_clause(solver &s, on_clause_eh_t &on_clause_eh)

handle add_soft(expr const &e, char const *weight)

void add(expr const &e, expr const &t)

expr lower(handle const &h)

expr_vector objectives() const

void add(expr_vector const &es)

void add(expr const &e, char const *p)

void set_initial_value(expr const &var, expr const &value)

handle add(expr const &e, unsigned weight)

check_result check(expr_vector const &asms)

void set_initial_value(expr const &var, int i)

friend std::ostream & operator<<(std::ostream &out, optimize const &s)

void set_initial_value(expr const &var, bool b)

handle add_soft(expr const &e, unsigned weight)

handle maximize(expr const &e)

optimize(optimize const &o)

void from_file(char const *filename)

expr_vector assertions() const

void from_string(char const *constraints)

expr upper(handle const &h)

optimize(context &c, optimize &src)

handle minimize(expr const &e)

optimize & operator=(optimize const &o)

void set(params const &p)

expr_vector unsat_core() const

param_descrs(param_descrs const &o)

param_descrs(context &c, Z3_param_descrs d)

Z3_param_kind kind(symbol const &s)

std::string documentation(symbol const &s)

static param_descrs simplify_param_descrs(context &c)

param_descrs & operator=(param_descrs const &o)

std::string to_string() const

static param_descrs global_param_descrs(context &c)

class for auxiliary parameters associated with func_decl The class is initialized with a func_decl or...

func_decl get_decl() const

std::string get_rational() const

symbol get_symbol() const

Z3_parameter_kind kind() const

double get_double() const

parameter(func_decl const &d, unsigned idx)

parameter(expr const &e, unsigned idx)

void set(char const *k, char const *s)

void set(char const *k, bool b)

void set(char const *k, unsigned n)

void set(char const *k, symbol const &s)

params & operator=(params const &s)

friend std::ostream & operator<<(std::ostream &out, params const &p)

void set(char const *k, double n)

friend probe operator<(probe const &p1, probe const &p2)

double operator()(goal const &g) const

probe & operator=(probe const &s)

friend probe operator==(probe const &p1, probe const &p2)

friend probe operator<=(probe const &p1, probe const &p2)

probe(context &c, Z3_probe s)

probe(context &c, double val)

probe(context &c, char const *name)

friend probe operator&&(probe const &p1, probe const &p2)

friend probe operator!(probe const &p)

double apply(goal const &g) const

friend probe operator>=(probe const &p1, probe const &p2)

friend probe operator>(probe const &p1, probe const &p2)

friend probe operator||(probe const &p1, probe const &p2)

simplifier & operator=(simplifier const &s)

simplifier(context &c, char const *name)

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

simplifier(context &c, Z3_simplifier s)

simplifier(simplifier const &s)

param_descrs get_param_descrs()

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

cube_generator(solver &s, expr_vector &vars)

cube_generator(solver &s)

void set_cutoff(unsigned c) noexcept

expr_vector const & operator*() const noexcept

bool operator==(cube_iterator const &other) const noexcept

cube_iterator & operator++()

cube_iterator operator++(int)

expr_vector const * operator->() const

bool operator!=(cube_iterator const &other) const noexcept

cube_iterator(solver &s, expr_vector &vars, unsigned &cutoff, bool end)

void from_string(char const *s)

cube_generator cubes(expr_vector &vars)

solver(context &c, solver const &src, translate)

expr_vector non_units() const

solver(context &c, simple)

solver(context &c, Z3_solver s)

solver(context &c, char const *logic)

void set(char const *k, bool v)

void add(expr const &e, expr const &p)

void add(expr const &e, char const *p)

check_result consequences(expr_vector &assumptions, expr_vector &vars, expr_vector &conseq)

void set_initial_value(expr const &var, expr const &value)

void set(char const *k, char const *v)

check_result check(unsigned n, expr *const assumptions)

std::string dimacs(bool include_names=true) const

expr_vector units() const

expr_vector trail() const

void set_initial_value(expr const &var, int i)

solver & operator=(solver const &s)

friend std::ostream & operator<<(std::ostream &out, solver const &s)

void set(char const *k, double v)

void push()

Create a backtracking point.

void set_initial_value(expr const &var, bool b)

std::string to_smt2(char const *status="unknown")

param_descrs get_param_descrs()

void set(char const *k, unsigned v)

void add(expr_vector const &v)

expr_vector assertions() const

void from_file(char const *file)

expr_vector trail(array< unsigned > &levels) const

std::string reason_unknown() const

void set(params const &p)

expr_vector cube(expr_vector &vars, unsigned cutoff)

expr_vector unsat_core() const

void set(char const *k, symbol const &v)

check_result check(expr_vector const &assumptions)

A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.

sort(context &c, Z3_sort s)

func_decl_vector constructors()

Z3_sort_kind sort_kind() const

Return the internal sort kind.

unsigned bv_size() const

Return the size of this Bit-vector sort.

bool is_int() const

Return true if this sort is the Integer sort.

bool is_real() const

Return true if this sort is the Real sort.

sort(context &c, Z3_ast a)

func_decl_vector recognizers()

symbol name() const

Return name of sort.

bool is_relation() const

Return true if this sort is a Relation sort.

unsigned fpa_ebits() const

sort array_range() const

Return the range of this Array sort.

bool is_bool() const

Return true if this sort is the Boolean sort.

bool is_arith() const

Return true if this sort is the Integer or Real sort.

bool is_bv() const

Return true if this sort is a Bit-vector sort.

sort array_domain() const

Return the domain of this Array sort.

bool is_finite_domain() const

Return true if this sort is a Finite domain sort.

bool is_datatype() const

Return true if this sort is a Datatype sort.

bool is_re() const

Return true if this sort is a regular expression sort.

unsigned id() const

retrieve unique identifier for func_decl.

friend std::ostream & operator<<(std::ostream &out, sort const &s)

bool is_array() const

Return true if this sort is a Array sort.

bool is_seq() const

Return true if this sort is a Sequence sort.

unsigned fpa_sbits() const

bool is_fpa() const

Return true if this sort is a Floating point sort.

bool is_uint(unsigned i) const

bool is_double(unsigned i) const

double double_value(unsigned i) const

unsigned uint_value(unsigned i) const

stats & operator=(stats const &s)

stats(context &c, Z3_stats e)

std::string key(unsigned i) const

friend std::ostream & operator<<(std::ostream &out, stats const &s)

friend std::ostream & operator<<(std::ostream &out, symbol const &s)

Z3_symbol_kind kind() const

symbol(context &c, Z3_symbol s)

friend tactic par_or(unsigned n, tactic const *tactics)

friend tactic par_and_then(tactic const &t1, tactic const &t2)

tactic & operator=(tactic const &s)

tactic(context &c, char const *name)

tactic(context &c, Z3_tactic s)

friend tactic repeat(tactic const &t, unsigned max)

friend tactic with(tactic const &t, params const &p)

apply_result apply(goal const &g) const

friend tactic operator&(tactic const &t1, tactic const &t2)

friend tactic try_for(tactic const &t, unsigned ms)

param_descrs get_param_descrs()

apply_result operator()(goal const &g) const

friend tactic operator|(tactic const &t1, tactic const &t2)

void register_decide(decide_eh_t &c)

bool propagate(expr_vector const &fixed, expr_vector const &lhs, expr_vector const &rhs, expr const &conseq)

void register_created(created_eh_t &c)

virtual ~user_propagator_base()

virtual void decide(expr const &, unsigned, bool)

virtual void eq(expr const &, expr const &)

void register_eq(eq_eh_t &f)

void add(expr const &e)

tracks e by a unique identifier that is returned by the call.

virtual void created(expr const &)

void register_final(final_eh_t &f)

register a callback on final-check. During the final check stage, all propagations have been processe...

virtual void pop(unsigned num_scopes)=0

virtual void fixed(expr const &, expr const &)

virtual user_propagator_base * fresh(context &ctx)=0

user_propagators created using fresh() are created during search and their lifetimes are restricted t...

void conflict(expr_vector const &fixed)

bool propagate(expr_vector const &fixed, expr const &conseq)

user_propagator_base(solver *s)

user_propagator_base(context &c)

void conflict(expr_vector const &fixed, expr_vector const &lhs, expr_vector const &rhs)

bool next_split(expr const &e, unsigned idx, Z3_lbool phase)

void register_fixed(fixed_eh_t &f)

register callbacks. Callbacks can only be registered with user_propagators that were created using a ...

Z3_ast Z3_API Z3_mk_exists_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)

Similar to Z3_mk_forall_const.

Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)

Pseudo-Boolean relations.

Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o)

Return the set of asserted formulas on the optimization context.

Z3_ast_kind

The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.

Z3_ast Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a)

Return the interpretation (i.e., assignment) of constant a in the model m. Return NULL,...

Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)

Create the integer type.

Z3_simplifier Z3_API Z3_simplifier_and_then(Z3_context c, Z3_simplifier t1, Z3_simplifier t2)

Return a simplifier that applies t1 to a given goal and t2 to every subgoal produced by t1.

Z3_ast Z3_API Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t)

Predicate indicating whether t is a floating-point number representing +oo or -oo.

Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2)

Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...

Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const *domain, Z3_sort range)

Create an array type with N arguments.

Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)

Bitwise xnor.

Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err)

Return a string describing the given error code.

Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d, unsigned idx)

Return the parameter type associated with a declaration.

bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)

Check if s is a sequence sort.

Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)

Bitwise nor.

Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a)

Return the denominator (as a numeral AST) of a numeral AST of sort Real.

Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p)

Return a probe that evaluates to "true" when p does not evaluate to true.

Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d)

Return declaration kind corresponding to declaration.

void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p)

Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p.

Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f)

Return the 'else' value of the given function interpretation.

Z3_ast Z3_API Z3_mk_char_to_bv(Z3_context c, Z3_ast ch)

Create a bit-vector (code point) from character.

Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)

Two's complement signed greater than or equal to.

void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)

Increment the reference counter of the given fixedpoint context.

Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p)

Return a tactic that applies t using the given set of parameters.

Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)

Create the constant array.

void Z3_API Z3_simplifier_inc_ref(Z3_context c, Z3_simplifier t)

Increment the reference counter of the given simplifier.

void Z3_API Z3_fixedpoint_add_rule(Z3_context c, Z3_fixedpoint d, Z3_ast rule, Z3_symbol name)

Add a universal Horn clause as a named rule. The horn_rule should be of the form:

Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2)

Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...

Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o)

Retrieve the unsat core for the last Z3_optimize_check The unsat core is a subset of the assumptions ...

Z3_sort Z3_API Z3_mk_char_sort(Z3_context c)

Create a sort for unicode characters.

Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty)

Create a numeral of a int, bit-vector, or finite-domain sort.

Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re)

Create the regular language [re].

Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)

Two's complement signed less than or equal to.

void Z3_API Z3_query_constructor(Z3_context c, Z3_constructor constr, unsigned num_fields, Z3_func_decl *constructor, Z3_func_decl *tester, Z3_func_decl accessors[])

Query constructor for declared functions.

Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)

Return the declaration of a constant or function application.

void Z3_API Z3_optimize_set_initial_value(Z3_context c, Z3_optimize o, Z3_ast v, Z3_ast val)

provide an initialization hint to the solver. The initialization hint is used to calibrate an initial...

void Z3_API Z3_del_context(Z3_context c)

Delete the given logical context.

Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])

Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs....

Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])

Create an AST node representing args[0] * ... * args[num_args-1].

Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d, unsigned idx)

Return the expression value associated with an expression parameter.

Z3_goal_prec

Z3 custom error handler (See Z3_set_error_handler).

Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s)

Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.

Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst)

Replace the first occurrence of src with dst in s.

Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p)

Convert a parameter description set into a string. This function is mainly used for printing the cont...

Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1)

Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size m+i,...

void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)

Set the given solver using the given parameters.

Z3_ast Z3_API Z3_mk_set_intersect(Z3_context c, unsigned num_args, Z3_ast const args[])

Take the intersection of a list of sets.

Z3_params Z3_API Z3_mk_params(Z3_context c)

Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many comp...

Z3_ast Z3_API Z3_mk_fpa_is_subnormal(Z3_context c, Z3_ast t)

Predicate indicating whether t is a subnormal floating-point number.

unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)

Return the number of parameters associated with a declaration.

Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)

Check for subsetness of sets.

Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)

Interface to simplifier.

Z3_ast Z3_API Z3_mk_int(Z3_context c, int v, Z3_sort ty)

Create a numeral of an int, bit-vector, or finite-domain sort.

Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t)

Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.

Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector variables, Z3_ast_vector consequences)

retrieve consequences from solver that determine values of the supplied function symbols.

Z3_ast_vector Z3_API Z3_fixedpoint_from_file(Z3_context c, Z3_fixedpoint f, Z3_string s)

Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context....

void Z3_API Z3_get_string_contents(Z3_context c, Z3_ast s, unsigned length, unsigned contents[])

Retrieve the unescaped string constant stored in s.

Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)

Unsigned less than or equal to.

Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)

Create the full set.

Z3_param_kind Z3_API Z3_param_descrs_get_kind(Z3_context c, Z3_param_descrs p, Z3_symbol n)

Return the kind associated with the given parameter name n.

Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)

Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.

bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t *i)

Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int64_t int....

void Z3_API Z3_add_rec_def(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast args[], Z3_ast body)

Define the body of a recursive function.

Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s)

Return the parameter description set for the given solver object.

Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)

Conversion of a floating-point term into a signed bit-vector.

Z3_ast Z3_API Z3_mk_true(Z3_context c)

Create an AST node representing true.

Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx)

Retrieve lower bound value or approximation for the i'th optimization objective.

Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[])

Take the union of a list of sets.

Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)

Retrieve the model for the last Z3_optimize_check.

void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r)

Increment the reference counter of the given Z3_apply_result object.

Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast default_value)

Create a fresh func_interp object, add it to a model for a specified function. It has reference count...

Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)

Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.

Z3_decl_kind

The different kinds of interpreted function kinds.

unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)

Alias for Z3_get_domain_size.

void Z3_API Z3_ast_vector_set(Z3_context c, Z3_ast_vector v, unsigned i, Z3_ast a)

Update position i of the AST vector v with the AST a.

Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)

Bitwise exclusive-or.

Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)

Convert a statistics into a string.

Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(Z3_context c, Z3_fixedpoint f)

Return the parameter description set for the given fixedpoint object.

Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)

Create the real type.

void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s)

Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives....

Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)

Create less than or equal to.

Z3_string Z3_API Z3_simplifier_get_help(Z3_context c, Z3_simplifier t)

Return a string containing a description of parameters accepted by the given simplifier.

bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g)

Return true if the given goal contains the formula false.

Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c, unsigned num_bound, Z3_app const bound[], Z3_ast body)

Create a lambda expression using a list of constants that form the set of bound variables.

Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)

Return a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1....

void Z3_API Z3_fixedpoint_update_rule(Z3_context c, Z3_fixedpoint d, Z3_ast a, Z3_symbol name)

Update a named rule. A rule with the same name must have been previously created.

void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)

Decrement the reference counter of the given solver.

Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)

Two's complement signed less than.

Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i)

Return the declaration of the i-th function in the given model.

Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s)

Return the length of the sequence s.

Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)

Create a numeral of a given sort.

unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e)

Return the number of arguments in a Z3_func_entry object.

Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)

Interface to simplifier.

Z3_symbol Z3_API Z3_get_decl_symbol_parameter(Z3_context c, Z3_func_decl d, unsigned idx)

Return the double value associated with an double parameter.

void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string str)

load solver assertions from a string.

Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a)

Return the numerator (as a numeral AST) of a numeral AST of sort Real.

Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)

Create an AST node representing - arg.

Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c)

Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.

Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2)

Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the...

Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])

Create an AST node representing args[0] and ... and args[num_args-1].

void Z3_API Z3_simplifier_dec_ref(Z3_context c, Z3_simplifier g)

Decrement the reference counter of the given simplifier.

void Z3_API Z3_interrupt(Z3_context c)

Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers,...

Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s)

Convert string to integer.

Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)

Floating-point subtraction.

void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a)

Add a new formula a to the given goal. The formula is split according to the following procedure that...

Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i)

Return the name of the parameter at given index i.

Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)

Return the value of this point.

bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a)

Determine if ast is an existential quantifier.

Z3_ast_vector Z3_API Z3_fixedpoint_from_string(Z3_context c, Z3_fixedpoint f, Z3_string s)

Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context....

Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)

Create a free (uninterpreted) type using the given name (symbol).

void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)

Backtrack one level.

Z3_ast Z3_API Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t)

Predicate indicating whether t is a normal floating-point number.

Z3_ast Z3_API Z3_mk_false(Z3_context c)

Create an AST node representing false.

Z3_sort Z3_API Z3_mk_datatype(Z3_context c, Z3_symbol name, unsigned num_constructors, Z3_constructor constructors[])

Create datatype, such as lists, trees, records, enumerations or unions of records....

Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s)

Check whether the assertions in a given solver are consistent or not.

Z3_ast Z3_API Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)

Conversion of a floating-point term into an unsigned bit-vector.

Z3_ast Z3_API Z3_mk_rotate_right(Z3_context c, unsigned i, Z3_ast t1)

Rotate bits of t1 to the right i times.

Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)

Standard two's complement multiplication.

Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index)

Retrieve from s the unit sequence positioned at position index. The sequence is empty if the index is...

Z3_model Z3_API Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m)

Convert a model of the formulas of a goal to a model of an original goal. The model may be null,...

void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr)

Reclaim memory allocated to constructor.

Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)

Two's complement signed greater than.

Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)

Convert the given AST node into a string.

Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re)

Create the complement of the regular language re.

Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint f)

Retrieve set of background assertions from fixedpoint context.

Z3_context Z3_API Z3_mk_context_rc(Z3_config c)

Create a context using the given configuration. This function is similar to Z3_mk_context....

unsigned Z3_API Z3_fpa_get_ebits(Z3_context c, Z3_sort s)

Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.

Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)

Return the set of asserted formulas on the solver.

Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t)

Create a new solver that is implemented using the given tactic. The solver supports the commands Z3_s...

Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg)

Take the complement of a set.

bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx)

Return true if the given statistical data is a unsigned integer.

bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx)

Return true if the given statistical data is a double.

Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c)

Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.

unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m)

Return the number of constants assigned by the given model.

Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision)

Return a lower bound for the given real algebraic number. The interval isolating the number is smalle...

Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1)

Extract the bits high down to low from a bit-vector of size m to yield a new bit-vector of size n,...

Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)

Create an AST node representing arg1 mod arg2.

Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1)

Take conjunction of bits in vector, return vector of length 1.

Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem)

Add an element to a set.

Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)

Create greater than or equal to.

Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)

Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.

Z3_ast Z3_API Z3_mk_fpa_rtp(Z3_context c)

Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.

void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value)

Set a value of a context parameter.

Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)

Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.

void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode)

Select mode for the format used for pretty-printing AST nodes.

bool Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback cb, unsigned num_fixed, Z3_ast const *fixed, unsigned num_eqs, Z3_ast const *eq_lhs, Z3_ast const *eq_rhs, Z3_ast conseq)

propagate a consequence based on fixed values and equalities. A client may invoke it during the pro...

unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s)

Retrieves the number of bits reserved for the significand in a FloatingPoint sort.

Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)

Create a universal quantifier using a list of constants that will form the set of bound variables.

Z3_param_kind

The different kinds of parameters that can be associated with parameter sets. (see Z3_mk_params).

const char * Z3_string

Z3 string type. It is just an alias for const char *.

Z3_constructor Z3_API Z3_mk_constructor(Z3_context c, Z3_symbol name, Z3_symbol recognizer, unsigned num_fields, Z3_symbol const field_names[], Z3_sort_opt const sorts[], unsigned sort_refs[])

Create a constructor.

Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t)

Return the parameter description set for the given tactic object.

Z3_sort Z3_API Z3_mk_tuple_sort(Z3_context c, Z3_symbol mk_tuple_name, unsigned num_fields, Z3_symbol const field_names[], Z3_sort const field_sorts[], Z3_func_decl *mk_tuple_decl, Z3_func_decl proj_decl[])

Create a tuple type.

Z3_ast_vector Z3_API Z3_ast_vector_translate(Z3_context s, Z3_ast_vector v, Z3_context t)

Translate the AST vector v from context s into an AST vector in context t.

void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e)

Increment the reference counter of the given Z3_func_entry object.

Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)

Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.

Z3_sort_kind

The different kinds of Z3 types (See Z3_get_sort_kind).

void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)

Create a backtracking point.

Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)

Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.

Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2)

Maximum of floating-point numbers.

void Z3_API Z3_optimize_assert_and_track(Z3_context c, Z3_optimize o, Z3_ast a, Z3_ast t)

Assert tracked hard constraint to the optimization context.

unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id)

Assert soft constraint to the optimization context.

Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)

Unsigned division.

Z3_string Z3_API Z3_ast_vector_to_string(Z3_context c, Z3_ast_vector v)

Convert AST vector into a string.

Z3_ast_vector Z3_API Z3_solver_get_trail(Z3_context c, Z3_solver s)

Return the trail modulo model conversion, in order of decision level The decision level can be retrie...

Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)

Shift left.

Z3_func_decl Z3_API Z3_mk_tree_order(Z3_context c, Z3_sort a, unsigned id)

create a tree ordering relation over signature a identified using index id.

Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2)

Two's complement signed remainder (sign follows dividend).

Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)

Declare a constant or function.

unsigned Z3_API Z3_goal_num_exprs(Z3_context c, Z3_goal g)

Return the number of formulas, subformulas and terms in the given goal.

Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic)

Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unkn...

Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)

Check if a real number is an integer.

void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, bool v)

Add a Boolean parameter k with value v to the parameter set p.

unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r)

Return the number of subgoals in the Z3_apply_result object returned by Z3_tactic_apply.

Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)

Create an AST node representing an if-then-else: ite(t1, t2, t3).

Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i)

Array read. The argument a is the array and i is the index of the array that gets read.

Z3_ast Z3_API Z3_mk_sign_ext(Z3_context c, unsigned i, Z3_ast t1)

Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of size m+i,...

Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)

Create a unit sequence of a.

Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[])

Create the intersection of the regular languages.

Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level)

extract a next cube for a solver. The last cube is the constant true or false. The number of (non-con...

Z3_ast Z3_API Z3_mk_u32string(Z3_context c, unsigned len, unsigned const chars[])

Create a string constant out of the string that is passed in It takes the length of the string as wel...

void Z3_API Z3_fixedpoint_add_fact(Z3_context c, Z3_fixedpoint d, Z3_func_decl r, unsigned num_args, unsigned args[])

Add a Database fact.

unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g)

Return the number of formulas in the given goal.

Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort *domain, Z3_sort range)

void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)

Increment the reference counter of the given statistics object.

Z3_ast Z3_API Z3_mk_select_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const *idxs)

n-ary Array read. The argument a is the array and idxs are the indices of the array that gets read.

Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a)

Return the coefficients of the defining polynomial.

Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)

Create an AST node representing arg1 div arg2.

Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)

Pseudo-Boolean relations.

Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq)

Create a regular expression sort out of a sequence sort.

Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)

Pseudo-Boolean relations.

void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)

Increment the reference counter of the given optimize context.

void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)

Decrement the reference counter of the given model.

Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative)

Create a floating-point infinity of sort s.

void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f)

Increment the reference counter of the given Z3_func_interp object.

Z3_func_decl Z3_API Z3_mk_piecewise_linear_order(Z3_context c, Z3_sort a, unsigned id)

create a piecewise linear ordering relation over signature a and index id.

void Z3_API Z3_params_set_double(Z3_context c, Z3_params p, Z3_symbol k, double v)

Add a double parameter k with value v to the parameter set p.

Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s)

Retrieve documentation string corresponding to parameter name s.

Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name)

create a forward reference to a recursive datatype being declared. The forward reference can be used ...

Z3_solver Z3_API Z3_mk_solver(Z3_context c)

Create a new solver. This solver is a "combined solver" (see combined_solver module) that internally ...

Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s)

Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.

int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s)

Return the symbol int value.

void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g)

Increment the reference counter of the given goal.

Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[])

Return a tactic that applies the given tactics in parallel.

Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)

Create an AST node representing t1 implies t2.

Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s)

Create a floating-point NaN of sort s.

unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t)

Return number of constructors for datatype.

Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx)

Retrieve upper bound value or approximation for the i'th optimization objective.

void Z3_API Z3_params_set_uint(Z3_context c, Z3_params p, Z3_symbol k, unsigned v)

Add a unsigned parameter k with value v to the parameter set p.

Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[])

Check whether the assertions in the given solver and optional assumptions are consistent or not.

Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2)

Floating-point greater than.

Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2)

Arithmetic shift right.

Z3_simplifier Z3_API Z3_simplifier_using_params(Z3_context c, Z3_simplifier t, Z3_params p)

Return a simplifier that applies t using the given set of parameters.

Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast t1, bool is_signed)

Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is t...

Z3_ast Z3_API Z3_mk_sbv_to_str(Z3_context c, Z3_ast s)

Signed bit-vector to string conversion.

Z3_ast Z3_API Z3_mk_fpa_is_zero(Z3_context c, Z3_ast t)

Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero.

Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem)

Remove an element to a set.

Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)

Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.

Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[])

Create the union of the regular languages.

Z3_param_descrs Z3_API Z3_simplifier_get_param_descrs(Z3_context c, Z3_simplifier t)

Return the parameter description set for the given simplifier object.

void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)

Set parameters on optimization context.

Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)

Bitwise or.

int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx)

Return the integer value associated with an integer parameter.

Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, unsigned idx)

Return idx'th constructor.

void Z3_API Z3_ast_vector_resize(Z3_context c, Z3_ast_vector v, unsigned n)

Resize the AST vector v.

Z3_lbool

Lifted Boolean type: false, undefined, true.

Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq)

Create an empty sequence of the sequence sort seq.

Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name)

Return a probe associated with the given name. The complete list of probes may be obtained using the ...

Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t)

Return a tactic that applies t to a given goal is the probe p evaluates to true. If p evaluates to fa...

Z3_ast Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s)

Check if suffix is a suffix of s.

Z3_symbol_kind Z3_API Z3_get_symbol_kind(Z3_context c, Z3_symbol s)

Return Z3_INT_SYMBOL if the symbol was constructed using Z3_mk_int_symbol, and Z3_STRING_SYMBOL if th...

void Z3_API Z3_solver_set_initial_value(Z3_context c, Z3_solver s, Z3_ast v, Z3_ast val)

provide an initialization hint to the solver. The initialization hint is used to calibrate an initial...

bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a)

Determine if ast is a lambda expression.

Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target)

Copy a solver s from the context source to the context target.

void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)

Create a backtracking point.

unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx)

Return the unsigned value of the given statistical data.

void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)

Increment the reference counter of the given probe.

Z3_sort Z3_API Z3_get_array_sort_domain(Z3_context c, Z3_sort t)

Return the domain of the given array sort. In the case of a multi-dimensional array,...

Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2)

Floating-point equality.

void Z3_API Z3_solver_propagate_register_cb(Z3_context c, Z3_solver_callback cb, Z3_ast e)

register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Ve...

Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)

Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflo...

bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t *u)

Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine uint64_t int....

void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a)

Add a constant interpretation.

Z3_string Z3_API Z3_sort_to_string(Z3_context c, Z3_sort s)

Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)

Standard two's complement addition.

unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a)

Return which root of the polynomial the algebraic number represents.

void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p)

Decrement the reference counter of the given parameter set.

void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)

Decrement the reference counter of the given fixedpoint context.

Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i)

Return the i-th argument of the given application.

Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)

Convert the given model into a string.

unsigned Z3_API Z3_get_string_length(Z3_context c, Z3_ast s)

Retrieve the length of the unescaped string constant stored in s.

Z3_string Z3_API Z3_tactic_get_help(Z3_context c, Z3_tactic t)

Return a string containing a description of parameters accepted by the given tactic.

void Z3_API Z3_solver_propagate_final(Z3_context c, Z3_solver s, Z3_final_eh final_eh)

register a callback on final check. This provides freedom to the propagator to delay actions or imple...

unsigned Z3_API Z3_param_descrs_size(Z3_context c, Z3_param_descrs p)

Return the number of parameters in the given parameter description set.

Z3_parameter_kind

The different kinds of parameters that can be associated with function symbols.

Z3_ast_vector Z3_API Z3_parse_smtlib2_string(Z3_context c, Z3_string str, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])

Parse the given string using the SMT-LIB2 parser.

Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2)

Floating-point greater than or equal.

Z3_ast Z3_API Z3_mk_bit2bool(Z3_context c, unsigned i, Z3_ast t1)

Extracts the bit at position i of a bit-vector and yields a boolean.

void Z3_API Z3_solver_register_on_clause(Z3_context c, Z3_solver s, void *user_context, Z3_on_clause_eh on_clause_eh)

register a callback to that retrieves assumed, inferred and deleted clauses during search.

Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g, bool include_names)

Convert a goal into a DIMACS formatted string. The goal must be in CNF. You can convert a goal to CNF...

Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)

Create less than.

double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx)

Return the double value of the given statistical data.

Z3_ast Z3_API Z3_mk_fpa_numeral_float(Z3_context c, float v, Z3_sort ty)

Create a numeral of FloatingPoint sort from a float.

Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)

Unsigned greater than.

Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query)

Pose a query against the asserted rules.

unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g)

Return the depth of the given goal. It tracks how many transformations were applied to it.

Z3_ast Z3_API Z3_mk_fpa_rtz(Z3_context c)

Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.

Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s)

Return the symbol name.

Z3_lbool Z3_API Z3_get_bool_value(Z3_context c, Z3_ast a)

Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise.

Z3_simplifier Z3_API Z3_mk_simplifier(Z3_context c, Z3_string name)

Return a simplifier associated with the given name. The complete list of simplifiers may be obtained ...

Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)

Bitwise negation.

Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)

Unsigned remainder.

Z3_ast Z3_API Z3_mk_seq_foldli(Z3_context c, Z3_ast f, Z3_ast i, Z3_ast a, Z3_ast s)

Create a fold with index tracking of the function f over the sequence s with accumulator a starting a...

void Z3_API Z3_mk_datatypes(Z3_context c, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort sorts[], Z3_constructor_list constructor_lists[])

Create mutually recursive datatypes.

Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s)

Return the set of non units in the solver state.

Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq)

Create a regular expression that accepts the sequence seq.

Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)

Standard two's complement subtraction.

Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o)

Return objectives on the optimization context. If the objective function is a max-sat objective it is...

Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset)

Return index of the first occurrence of substr in s starting from offset offset. If s does not contai...

Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision)

Return a upper bound for the given real algebraic number. The interval isolating the number is smalle...

Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)

Create an AST node representing arg1 ^ arg2.

Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])

Concatenate sequences.

Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, Z3_symbol name, unsigned n, Z3_symbol const enum_names[], Z3_func_decl enum_consts[], Z3_func_decl enum_testers[])

Create a enumeration sort.

Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi)

Create the range regular expression over two sequences of length 1.

unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t)

Return the size of the given bit-vector sort.

Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)

Retrieve set of rules from fixedpoint context.

Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set)

Check for set membership.

void Z3_API Z3_ast_vector_dec_ref(Z3_context c, Z3_ast_vector v)

Decrement the reference counter of the given AST vector.

Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p)

Return a tactic that fails if the probe p evaluates to false.

void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g)

Erase all formulas from the given goal.

void Z3_API Z3_func_interp_dec_ref(Z3_context c, Z3_func_interp f)

Decrement the reference counter of the given Z3_func_interp object.

void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)

Decrement the reference counter of the given probe.

void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p)

Increment the reference counter of the given parameter set.

void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)

Register a Z3 error handler.

Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])

Create an AST node representing distinct(args[0], ..., args[num_args-1]).

Z3_ast Z3_API Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s)

Check if prefix is a prefix of s.

Z3_config Z3_API Z3_mk_config(void)

Create a configuration object for the Z3 context object.

void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value)

Set a configuration parameter.

Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)

Create a bit-vector type of the given size.

Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)

Floating-point remainder.

Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)

Unsigned less than.

Z3_probe Z3_API Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2)

Return a probe that evaluates to "true" when p1 or p2 evaluates to true.

Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)

Create a new fixedpoint context.

Z3_string Z3_API Z3_params_to_string(Z3_context c, Z3_params p)

Convert a parameter set into a string. This function is mainly used for printing the contents of a pa...

Z3_param_descrs Z3_API Z3_get_global_param_descrs(Z3_context c)

Retrieve description of global parameters.

void Z3_API Z3_solver_propagate_init(Z3_context c, Z3_solver s, void *user_context, Z3_push_eh push_eh, Z3_pop_eh pop_eh, Z3_fresh_eh fresh_eh)

register a user-propagator with the solver.

Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i)

Return the i-th constant in the given model.

void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g)

Decrement the reference counter of the given tactic.

Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)

Bitwise nand.

Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)

Create a new incremental solver.

Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)

Return the range of the given declaration.

void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value)

Set a global (or module) parameter. This setting is shared by all Z3 contexts.

void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)

Assert hard constraint to the optimization context.

Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c, Z3_string name, Z3_string logic, Z3_string status, Z3_string attributes, unsigned num_assumptions, Z3_ast const assumptions[], Z3_ast formula)

Convert the given benchmark into SMT-LIB formatted string.

Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re)

Create the regular language re*.

Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, bool const *bits)

create a bit-vector numeral from a vector of Booleans.

void Z3_API Z3_func_entry_dec_ref(Z3_context c, Z3_func_entry e)

Decrement the reference counter of the given Z3_func_entry object.

unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)

Return the number of statistical data in s.

Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)

Print the current context as a string.

Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)

Return body of quantifier.

void Z3_API Z3_param_descrs_dec_ref(Z3_context c, Z3_param_descrs p)

Decrement the reference counter of the given parameter description set.

Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re)

Create an universal regular expression of sort re.

Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2)

Minimum of floating-point numbers.

Z3_model Z3_API Z3_mk_model(Z3_context c)

Create a fresh model object. It has reference count 0.

Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d)

Return the constant declaration name as a symbol.

Z3_ast Z3_API Z3_mk_seq_mapi(Z3_context c, Z3_ast f, Z3_ast i, Z3_ast s)

Create a map of the function f over the sequence s starting at index i.

Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1)

Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.

Z3_ast Z3_API Z3_mk_fpa_round_to_integral(Z3_context c, Z3_ast rm, Z3_ast t)

Floating-point roundToIntegral. Rounds a floating-point number to the closest integer,...

Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx)

Return the key (a string) for a particular statistical data.

Z3_ast Z3_API Z3_mk_re_diff(Z3_context c, Z3_ast re1, Z3_ast re2)

Create the difference of regular expressions.

unsigned Z3_API Z3_fixedpoint_get_num_levels(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred)

Query the PDR engine for the maximal levels properties are known about predicate.

Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t v, Z3_sort ty)

Create a numeral of a int, bit-vector, or finite-domain sort.

Z3_symbol_kind

The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See Z3_...

Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re)

Create an empty regular expression of sort re.

Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)

Floating-point addition.

Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)

Bitwise and.

Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)

Return the parameter description set for the simplify procedure.

bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g)

Return true if the goal contains false, and it is precise or the product of an over approximation.

Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])

Create an AST node representing args[0] + ... + args[num_args-1].

Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)

Return the kind of the given AST.

Z3_ast_vector Z3_API Z3_parse_smtlib2_file(Z3_context c, Z3_string file_name, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])

Similar to Z3_parse_smtlib2_string, but reads the benchmark from a file.

Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)

Two's complement signed remainder (sign follows divisor).

Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2)

Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluat...

Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst)

translate model from context c to context dst.

Z3_string Z3_API Z3_fixedpoint_to_string(Z3_context c, Z3_fixedpoint f, unsigned num_queries, Z3_ast queries[])

Print the current rules and background axioms as a string.

void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[])

retrieve the decision depth of Boolean literals (variables or their negations). Assumes a check-sat c...

Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)

Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)

Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.

Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1)

Create an n bit bit-vector from the integer argument t1.

void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)

Assert a constraint into the solver.

Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name)

Return a tactic associated with the given name. The complete list of tactics may be obtained using th...

Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)

Floating-point absolute value.

unsigned Z3_API Z3_ast_vector_size(Z3_context c, Z3_ast_vector v)

Return the size of the given AST vector.

Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)

Create a new optimize context.

bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast *v)

Evaluate the AST node t in the given model. Return true if succeeded, and store the result in v.

Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t)

Return the range of the given array sort.

void Z3_API Z3_del_constructor_list(Z3_context c, Z3_constructor_list clist)

Reclaim memory allocated for constructor list.

Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty)

Create a variable.

unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a)

Return the number of argument of an application. If t is an constant, then the number of arguments is...

Z3_ast Z3_API Z3_substitute_funs(Z3_context c, Z3_ast a, unsigned num_funs, Z3_func_decl const from[], Z3_ast const to[])

Substitute functions in from with new expressions in to.

Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i)

Return an argument of a Z3_func_entry object.

Z3_error_code

Z3 error codes (See Z3_get_error_code).

Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)

Create an AST node representing l = r.

Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)

Pseudo-Boolean relations.

void Z3_API Z3_ast_vector_inc_ref(Z3_context c, Z3_ast_vector v)

Increment the reference counter of the given AST vector.

unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m)

Return the number of function interpretations in the given model.

void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a)

Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...

Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s)

Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the as...

Z3_ast_vector Z3_API Z3_mk_ast_vector(Z3_context c)

Return an empty AST vector.

void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)

Decrement the reference counter of the given optimize context.

Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s)

Retrieve the string constant stored in s. Characters outside the basic printable ASCII range are esca...

Z3_ast Z3_API Z3_mk_fpa_is_nan(Z3_context c, Z3_ast t)

Predicate indicating whether t is a NaN.

bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int *i)

Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int....

Z3_error_code Z3_API Z3_get_error_code(Z3_context c)

Return the error code for the last API call.

Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig)

Create an expression of FloatingPoint sort from three bit-vector expressions.

Z3_func_decl Z3_API Z3_mk_partial_order(Z3_context c, Z3_sort a, unsigned id)

create a partial ordering relation over signature a and index id.

Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)

Create the empty set.

bool Z3_API Z3_is_string(Z3_context c, Z3_ast s)

Determine if s is a string constant.

Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi)

Create a regular expression loop. The supplied regular expression r is repeated between lo and hi tim...

Z3_ast Z3_API Z3_mk_char_to_int(Z3_context c, Z3_ast ch)

Create an integer (code point) from character.

Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)

Floating-point negation.

Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)

Repeat the given bit-vector up length i.

Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re)

Create the regular language re+.

Z3_goal_prec Z3_API Z3_goal_precision(Z3_context c, Z3_goal g)

Return the "precision" of the given goal. Goals can be transformed using over and under approximation...

void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)

Backtrack n backtracking points.

Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)

Coerce an integer to a real.

Z3_goal Z3_API Z3_mk_goal(Z3_context c, bool models, bool unsat_cores, bool proofs)

Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or trans...

double Z3_API Z3_get_decl_double_parameter(Z3_context c, Z3_func_decl d, unsigned idx)

Return the double value associated with an double parameter.

unsigned Z3_API Z3_get_ast_hash(Z3_context c, Z3_ast a)

Return a hash code for the given AST. The hash code is structural but two different AST objects can m...

Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2)

Floating-point less than.

Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, uint64_t v, Z3_sort ty)

Create a numeral of a int, bit-vector, or finite-domain sort.

Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t)

Return a string containing a description of parameters accepted by optimize.

Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d)

Return the sort name as a symbol.

Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(Z3_context c, Z3_sort t, unsigned idx)

Return idx'th recognizer.

void Z3_API Z3_global_param_reset_all(void)

Restore the value of all global (and module) parameters. This command will not affect already created...

Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)

Create greater than.

Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d)

Retrieve statistics information from the last call to Z3_optimize_check.

Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v)

Array update.

Z3_probe Z3_API Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2)

Return a probe that evaluates to "true" when the value returned by p1 is greater than the value retur...

Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s)

Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.

Z3_string Z3_API Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d, unsigned idx)

Return the rational value, as a string, associated with a rational parameter.

unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)

Add a minimization constraint.

Z3_stats Z3_API Z3_fixedpoint_get_statistics(Z3_context c, Z3_fixedpoint d)

Retrieve statistics information from the last call to Z3_fixedpoint_query.

bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a)

Test if there exists an interpretation (i.e., assignment) for a in the model m.

void Z3_API Z3_ast_vector_push(Z3_context c, Z3_ast_vector v, Z3_ast a)

Add the AST a in the end of the AST vector v. The size of v is increased by one.

bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)

Compare terms.

bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)

Determine if an ast is a universal quantifier.

void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)

Increment the reference counter of the given tactic.

Z3_ast Z3_API Z3_mk_real_int64(Z3_context c, int64_t num, int64_t den)

Create a real from a fraction of int64.

void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name)

load solver assertions from a file.

Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast s, Z3_ast substr)

Return index of the last occurrence of substr in s. If s does not contain substr, then the value is -...

Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)

Create an AST node representing t1 xor t2.

void Z3_API Z3_solver_propagate_eq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh)

register a callback on expression equalities.

Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s)

Create a string constant out of the string that is passed in The string may contain escape encoding f...

Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f)

create transitive closure of binary relation.

Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms)

Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms mil...

Z3_ast Z3_API Z3_mk_rotate_left(Z3_context c, unsigned i, Z3_ast t1)

Rotate bits of t1 to the left i times.

void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r)

Decrement the reference counter of the given Z3_apply_result object.

Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s)

Create a sequence sort out of the sort for the elements.

unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)

Add a maximization constraint.

Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)

Return the set of units modulo model conversion.

Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)

Declare and create a constant.

Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)

Create a Z3 symbol using a C string.

void Z3_API Z3_param_descrs_inc_ref(Z3_context c, Z3_param_descrs p)

Increment the reference counter of the given parameter description set.

Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i)

Return one of the subgoals in the Z3_apply_result object returned by Z3_tactic_apply.

Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2)

Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...

void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)

Decrement the reference counter of the given statistics object.

Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])

Create the concatenation of the regular languages.

Z3_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i)

Return a "point" of the given function interpretation. It represents the value of f in a particular p...

Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)

Declare a recursive function.

unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t)

Return a unique identifier for t. The identifier is unique up to structural equality....

Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)

Concatenate the given bit-vectors.

Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)

Conversion of a FloatingPoint term into another term of different FloatingPoint sort.

Z3_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, unsigned idx)

Return the sort value associated with a sort parameter.

Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c, unsigned num_constructors, Z3_constructor const constructors[])

Create list of constructors.

Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)

Apply tactic t to the goal g.

Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)

Floating-point less than or equal.

void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh)

register a callback when a new expression with a registered function is used by the solver The regist...

Z3_ast Z3_API Z3_mk_fpa_numeral_double(Z3_context c, double v, Z3_sort ty)

Create a numeral of FloatingPoint sort from a double.

unsigned Z3_API Z3_get_sort_id(Z3_context c, Z3_sort s)

Return a unique identifier for s.

Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)

Floating-point multiplication.

Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])

Create a constant or function application.

Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t)

Return the sort kind (e.g., array, tuple, int, bool, etc).

Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)

Return statistics for the given solver.

Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)

Standard two's complement unary minus.

Z3_ast Z3_API Z3_mk_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const *idxs, Z3_ast v)

n-ary Array update.

Z3_string Z3_API Z3_fixedpoint_get_reason_unknown(Z3_context c, Z3_fixedpoint d)

Retrieve a string that describes the last status returned by Z3_fixedpoint_query.

Z3_func_decl Z3_API Z3_mk_linear_order(Z3_context c, Z3_sort a, unsigned id)

create a linear ordering relation over signature a. The relation is identified by the index id.

Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f)

Return a string describing all fixedpoint available parameters.

Z3_sort Z3_API Z3_get_domain(Z3_context c, Z3_func_decl d, unsigned i)

Return the sort of the i-th parameter of the given function declaration.

Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re)

Check if seq is in the language generated by the regular expression re.

Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)

Create the Boolean type.

Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])

Create an AST node representing args[0] - ... - args[num_args - 1].

void Z3_API Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v)

Add a symbol parameter k with value v to the parameter set p.

Z3_ast Z3_API Z3_ast_vector_get(Z3_context c, Z3_ast_vector v, unsigned i)

Return the AST at position i in the AST vector v.

Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s, bool include_names)

Convert a solver into a DIMACS formatted string.

unsigned Z3_API Z3_get_func_decl_id(Z3_context c, Z3_func_decl f)

Return a unique identifier for f.

Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2)

Take the set difference between two sets.

void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh)

register a callback when the solver decides to split on a registered expression. The callback may cha...

Z3_ast Z3_API Z3_mk_lstring(Z3_context c, unsigned len, Z3_string s)

Create a string constant out of the string that is passed in It takes the length of the string as wel...

Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)

Two's complement signed division.

Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)

Logical shift right.

Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx)

Return the expression value associated with an expression parameter.

double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g)

Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0....

void Z3_API Z3_func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value)

Return the 'else' value of the given function interpretation.

void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g)

Decrement the reference counter of the given goal.

Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)

Create an AST node representing not(a).

void Z3_API Z3_solver_propagate_register(Z3_context c, Z3_solver s, Z3_ast e)

register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Ve...

Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])

Substitute the variables in a with the expressions in to. For every i smaller than num_exprs,...

Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])

Create an AST node representing args[0] or ... or args[num_args-1].

Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)

Create an array type.

Z3_tactic Z3_API Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2)

Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 appl...

void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m)

Increment the reference counter of the given model.

Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length)

Extract subsequence starting at offset of length.

Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)

Floating-point division.

Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)

Create a FloatingPoint sort.

Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)

Floating-point square root.

bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g)

Return true if the goal is empty, and it is precise or the product of a under approximation.

void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)

Set parameters on fixedpoint context.

void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s)

Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives....

Z3_solver Z3_API Z3_solver_add_simplifier(Z3_context c, Z3_solver solver, Z3_simplifier simplifier)

Attach simplifier to a solver. The solver will use the simplifier for incremental pre-processing.

Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)

Create an AST node representing arg1 rem arg2.

Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d)

Retrieve a formula that encodes satisfying answers to the query.

Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s)

Integer to string conversion.

bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned *u)

Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned int....

Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)

Return numeral value, as a decimal string of a numeric constant term.

void Z3_API Z3_solver_propagate_fixed(Z3_context c, Z3_solver s, Z3_fixed_eh fixed_eh)

register a callback for when an expression is bound to a fixed value. The supported expression types ...

Z3_ast Z3_API Z3_mk_seq_map(Z3_context c, Z3_ast f, Z3_ast s)

Create a map of the function f over the sequence s.

void Z3_API Z3_fixedpoint_register_relation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f)

Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics...

Z3_ast Z3_API Z3_mk_char_is_digit(Z3_context c, Z3_ast ch)

Create a check if the character is a digit.

void Z3_API Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property)

Add property about the predicate pred. Add a property of predicate pred at level. It gets pushed forw...

void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value)

add a function entry to a function interpretation.

bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)

Return true if the given expression t is well sorted.

Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)

Unsigned greater than or equal to.

Z3_lbool Z3_API Z3_fixedpoint_query_relations(Z3_context c, Z3_fixedpoint d, unsigned num_relations, Z3_func_decl const relations[])

Pose multiple queries against the asserted rules.

Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f)

Create array with the same interpretation as a function. The array satisfies the property (f x) = (se...

Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r)

Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.

Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)

Convert a solver into a string.

Z3_ast Z3_API Z3_mk_seq_foldl(Z3_context c, Z3_ast f, Z3_ast a, Z3_ast s)

Create a fold of the function f over the sequence s with accumulator a.

Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s)

Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...

Z3_ast Z3_API Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3)

Floating-point fused multiply-add.

Z3_string Z3_API Z3_get_numeral_binary_string(Z3_context c, Z3_ast a)

Return numeral value, as a binary string of a numeric constant term.

Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max)

Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of...

Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx)

Return a formula from the given goal.

Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[])

Check consistency and produce optimal values.

Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)

Create a Z3 symbol using an integer.

Z3_ast Z3_API Z3_mk_char_from_bv(Z3_context c, Z3_ast bv)

Create a character from a bit-vector (code point).

unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f)

Return the number of entries in the given function interpretation.

Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)

Return a probe that always evaluates to val.

Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c)

Create the RoundingMode sort.

Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g)

Convert a goal into a string.

Z3_ast Z3_API Z3_mk_fpa_rne(Z3_context c)

Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.

Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)

Pseudo-Boolean relations.

void Z3_API Z3_del_config(Z3_config c)

Delete the given configuration object.

double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a)

Return numeral as a double.

void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a)

Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...

Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)

Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1.

Z3_func_interp Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f)

Return the interpretation of the function f in the model m. Return NULL, if the model does not assign...

void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)

Increment the reference counter of the given solver.

bool Z3_API Z3_solver_next_split(Z3_context c, Z3_solver_callback cb, Z3_ast t, unsigned idx, Z3_lbool phase)

Z3_probe Z3_API Z3_probe_and(Z3_context x, Z3_probe p1, Z3_probe p2)

Return a probe that evaluates to "true" when p1 and p2 evaluates to true.

bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)

Check if s is a regular expression sort.

Z3_ast Z3_API Z3_mk_ubv_to_str(Z3_context c, Z3_ast s)

Unsigned bit-vector to string conversion.

Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)

Create a sort for unicode strings.

Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision)

Return numeral as a string in decimal notation. The result has at most precision decimal places.

Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)

Return the sort of an AST node.

Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(Z3_context c, Z3_sort t, unsigned idx_c, unsigned idx_a)

Return idx_a'th accessor for the idx_c'th constructor.

Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)

Take disjunction of bits in vector, return vector of length 1.

Z3_ast Z3_API Z3_mk_seq_nth(Z3_context c, Z3_ast s, Z3_ast index)

Retrieve from s the element positioned at position index. The function is under-specified if the inde...

Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)

Check if container contains containee.

void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)

Remove all assertions from the solver.

bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a)

Return true if the given AST is a real algebraic number.

@ Z3_PRINT_SMTLIB2_COMPLIANT

System.IntPtr Z3_ast_vector

System.IntPtr Z3_func_interp

System.IntPtr Z3_func_decl

System.IntPtr Z3_func_entry

System.IntPtr Z3_solver_callback

expr re_intersect(expr_vector const &args)

expr indexof(expr const &s, expr const &substr, expr const &offset)

expr mk_and(expr_vector const &args)

expr fpa_to_ubv(expr const &t, unsigned sz)

expr star(expr const &re)

void check_context(object const &a, object const &b)

expr bvsub_no_overflow(expr const &a, expr const &b)

expr operator==(expr const &a, expr const &b)

expr operator>=(expr const &a, expr const &b)

expr srem(expr const &a, expr const &b)

signed remainder operator for bitvectors

expr bvadd_no_underflow(expr const &a, expr const &b)

expr pble(expr_vector const &es, int const *coeffs, int bound)

expr store(expr const &a, expr const &i, expr const &v)

expr mod(expr const &a, expr const &b)

expr fma(expr const &a, expr const &b, expr const &c, expr const &rm)

expr range(expr const &lo, expr const &hi)

expr round_fpa_to_closest_integer(expr const &t)

expr distinct(expr_vector const &args)

expr bvmul_no_underflow(expr const &a, expr const &b)

expr operator|(expr const &a, expr const &b)

expr pbeq(expr_vector const &es, int const *coeffs, int bound)

ast_vector_tpl< func_decl > func_decl_vector

expr lshr(expr const &a, expr const &b)

logic shift right operator for bitvectors

expr bv2int(expr const &a, bool is_signed)

bit-vector and integer conversions.

std::function< void(expr const &proof, std::vector< unsigned > const &deps, expr_vector const &clause)> on_clause_eh_t

expr max(expr const &a, expr const &b)

expr operator^(expr const &a, expr const &b)

func_decl linear_order(sort const &a, unsigned index)

expr operator<(expr const &a, expr const &b)

expr set_intersect(expr const &a, expr const &b)

func_decl tree_order(sort const &a, unsigned index)

expr forall(expr const &x, expr const &b)

expr bvneg_no_overflow(expr const &a)

expr set_member(expr const &s, expr const &e)

expr set_difference(expr const &a, expr const &b)

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

expr sext(expr const &a, unsigned i)

Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i,...

expr mapi(expr const &f, expr const &i, expr const &list)

expr bvadd_no_overflow(expr const &a, expr const &b, bool is_signed)

bit-vector overflow/underflow checks

expr slt(expr const &a, expr const &b)

signed less than operator for bitvectors.

expr bvsdiv_no_overflow(expr const &a, expr const &b)

expr empty_set(sort const &s)

expr plus(expr const &re)

expr rem(expr const &a, expr const &b)

expr re_diff(expr const &a, expr const &b)

expr operator!(expr const &a)

expr fpa_fp(expr const &sgn, expr const &exp, expr const &sig)

expr foldli(expr const &f, expr const &i, expr const &a, expr const &list)

expr mk_xor(expr_vector const &args)

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

expr full_set(sort const &s)

ast_vector_tpl< sort > sort_vector

expr as_array(func_decl &f)

tactic when(probe const &p, tactic const &t)

expr operator*(expr const &a, expr const &b)

expr uge(expr const &a, expr const &b)

unsigned greater than or equal to operator for bitvectors.

expr nand(expr const &a, expr const &b)

expr zext(expr const &a, unsigned i)

Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i,...

expr is_int(expr const &e)

expr empty(sort const &s)

expr operator-(expr const &a)

expr re_complement(expr const &a)

expr set_del(expr const &s, expr const &e)

expr mk_or(expr_vector const &args)

expr concat(expr const &a, expr const &b)

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

expr operator%(expr const &a, expr const &b)

expr re_full(sort const &s)

func_decl partial_order(sort const &a, unsigned index)

std::ostream & operator<<(std::ostream &out, exception const &e)

tactic par_and_then(tactic const &t1, tactic const &t2)

bool eq(ast const &a, ast const &b)

expr operator~(expr const &a)

expr exists(expr const &x, expr const &b)

expr ite(expr const &c, expr const &t, expr const &e)

Create the if-then-else expression ite(c, t, e)

expr bvsub_no_underflow(expr const &a, expr const &b, bool is_signed)

expr set_add(expr const &s, expr const &e)

expr sum(expr_vector const &args)

expr last_indexof(expr const &s, expr const &substr)

expr pbge(expr_vector const &es, int const *coeffs, int bound)

expr set_union(expr const &a, expr const &b)

func_decl to_func_decl(context &c, Z3_func_decl f)

tactic cond(probe const &p, tactic const &t1, tactic const &t2)

expr sbv_to_fpa(expr const &t, sort s)

expr ubv_to_fpa(expr const &t, sort s)

expr operator||(expr const &a, expr const &b)

expr const_array(sort const &d, expr const &v)

tactic par_or(unsigned n, tactic const *tactics)

func_decl piecewise_linear_order(sort const &a, unsigned index)

expr operator&&(expr const &a, expr const &b)

func_decl function(std::string const &name, sort_vector const &domain, sort const &range)

expr atleast(expr_vector const &es, unsigned bound)

expr atmost(expr_vector const &es, unsigned bound)

expr operator>(expr const &a, expr const &b)

tactic repeat(tactic const &t, unsigned max=UINT_MAX)

expr re_empty(sort const &s)

expr select(expr const &a, expr const &i)

forward declarations

expr urem(expr const &a, expr const &b)

unsigned reminder operator for bitvectors

expr in_re(expr const &s, expr const &re)

expr to_re(expr const &s)

expr operator/(expr const &a, expr const &b)

expr fp_eq(expr const &a, expr const &b)

expr bvredor(expr const &a)

expr nor(expr const &a, expr const &b)

expr bvmul_no_overflow(expr const &a, expr const &b, bool is_signed)

expr min(expr const &a, expr const &b)

expr sle(expr const &a, expr const &b)

signed less than or equal to operator for bitvectors.

sort to_sort(context &c, Z3_sort s)

check_result to_check_result(Z3_lbool l)

expr ugt(expr const &a, expr const &b)

unsigned greater than operator for bitvectors.

ast_vector_tpl< expr > expr_vector

expr sgt(expr const &a, expr const &b)

signed greater than operator for bitvectors.

expr lambda(expr const &x, expr const &b)

expr to_real(expr const &a)

expr foldl(expr const &f, expr const &a, expr const &list)

expr operator+(expr const &a, expr const &b)

expr int2bv(unsigned n, expr const &a)

expr udiv(expr const &a, expr const &b)

unsigned division operator for bitvectors.

expr prefixof(expr const &a, expr const &b)

expr suffixof(expr const &a, expr const &b)

expr set_complement(expr const &a)

expr fpa_to_sbv(expr const &t, unsigned sz)

expr ule(expr const &a, expr const &b)

unsigned less than or equal to operator for bitvectors.

expr operator<=(expr const &a, expr const &b)

expr option(expr const &re)

expr to_expr(context &c, Z3_ast a)

Wraps a Z3_ast as an expr object. It also checks for errors. This function allows the user to use the...

expr operator!=(expr const &a, expr const &b)

tactic fail_if(probe const &p)

ast_vector_tpl< ast > ast_vector

expr map(expr const &f, expr const &list)

expr sqrt(expr const &a, expr const &rm)

expr shl(expr const &a, expr const &b)

shift left operator for bitvectors

expr implies(expr const &a, expr const &b)

expr operator&(expr const &a, expr const &b)

expr sge(expr const &a, expr const &b)

signed greater than or equal to operator for bitvectors.

expr smod(expr const &a, expr const &b)

signed modulus operator for bitvectors

expr set_subset(expr const &a, expr const &b)

expr ult(expr const &a, expr const &b)

unsigned less than operator for bitvectors.

expr pw(expr const &a, expr const &b)

expr ashr(expr const &a, expr const &b)

arithmetic shift right operator for bitvectors

expr xnor(expr const &a, expr const &b)

expr bvredand(expr const &a)

tactic try_for(tactic const &t, unsigned ms)

expr fpa_to_fpa(expr const &t, sort s)

def on_clause_eh(ctx, p, n, dep, clause)

#define _Z3_MK_BIN_(a, b, binop)

#define MK_EXPR1(_fn, _arg)

#define MK_EXPR2(_fn, _arg1, _arg2)

#define _Z3_MK_UN_(a, mkun)

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4