mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

Merge branch 'unstable' into contrib

Browse source
This commit is contained in:
Leonardo de Moura 2013-06-05 14:00:59 -07:00
commit d2a2dbb4b6
230 changed files with 9263 additions and 13830 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/api/api_ast.cpp
View file

@ -46,7 +46,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_int_symbol(c, i);
RESET_ERROR_CODE();
if (i < 0 || (unsigned)i >= (SIZE_MAX >> PTR_ALIGNMENT)) {
if (i < 0 || (size_t)i >= (SIZE_MAX >> PTR_ALIGNMENT)) {
SET_ERROR_CODE(Z3_IOB);
return 0;
}
@ -1070,6 +1070,10 @@ extern "C" {
case OP_BV2INT: return Z3_OP_BV2INT;
case OP_CARRY: return Z3_OP_CARRY;
case OP_XOR3: return Z3_OP_XOR3;
case OP_BSMUL_NO_OVFL:
case OP_BUMUL_NO_OVFL:
case OP_BSMUL_NO_UDFL:
return Z3_OP_UNINTERPRETED;
default:
UNREACHABLE();
return Z3_OP_UNINTERPRETED;

133
src/api/api_bv.cpp
View file

@ -121,10 +121,20 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
unsigned sz = Z3_get_bv_sort_size(c, s);
rational max_bound = power(rational(2), sz);
Z3_ast bound = Z3_mk_numeral(c, max_bound.to_string().c_str(), int_s);
Z3_ast pred = Z3_mk_bvslt(c, n, Z3_mk_int(c, 0, s));
Z3_inc_ref(c, bound);
Z3_ast zero = Z3_mk_int(c, 0, s);
Z3_inc_ref(c, zero);
Z3_ast pred = Z3_mk_bvslt(c, n, zero);
Z3_inc_ref(c, pred);
// if n <_sigend 0 then r - s^sz else r
Z3_ast args[2] = { r, bound };
Z3_ast res = Z3_mk_ite(c, pred, Z3_mk_sub(c, 2, args), r);
Z3_ast sub = Z3_mk_sub(c, 2, args);
Z3_inc_ref(c, sub);
Z3_ast res = Z3_mk_ite(c, pred, sub, r);
Z3_dec_ref(c, bound);
Z3_dec_ref(c, pred);
Z3_dec_ref(c, sub);
Z3_dec_ref(c, zero);
RETURN_Z3(res);
}
else {
@ -156,7 +166,14 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
return Z3_mk_bvshl(c, Z3_mk_int64(c, 1, s), Z3_mk_int64(c, sz - 1, s));
Z3_ast x = Z3_mk_int64(c, 1, s);
Z3_inc_ref(c, x);
Z3_ast y = Z3_mk_int64(c, sz - 1, s);
Z3_inc_ref(c, y);
Z3_ast result = Z3_mk_bvshl(c, x, y);
Z3_dec_ref(c, x);
Z3_dec_ref(c, y);
return result;
Z3_CATCH_RETURN(0);
}
@ -177,17 +194,40 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
RESET_ERROR_CODE();
if (is_signed) {
Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1));
Z3_inc_ref(c, zero);
Z3_ast r = Z3_mk_bvadd(c, t1, t2);
Z3_ast args[2] = { Z3_mk_bvslt(c, zero, t1), Z3_mk_bvslt(c, zero, t2) };
Z3_inc_ref(c, r);
Z3_ast l1 = Z3_mk_bvslt(c, zero, t1);
Z3_inc_ref(c, l1);
Z3_ast l2 = Z3_mk_bvslt(c, zero, t2);
Z3_inc_ref(c, l2);
Z3_ast args[2] = { l1, l2 };
Z3_ast args_pos = Z3_mk_and(c, 2, args);
return Z3_mk_implies(c, args_pos, Z3_mk_bvslt(c, zero, r));
Z3_inc_ref(c, args_pos);
Z3_ast result = Z3_mk_implies(c, args_pos, Z3_mk_bvslt(c, zero, r));
Z3_dec_ref(c, r);
Z3_dec_ref(c, l1);
Z3_dec_ref(c, l2);
Z3_dec_ref(c, args_pos);
Z3_dec_ref(c, zero);
return result;
}
else {
unsigned sz = Z3_get_bv_sort_size(c, Z3_get_sort(c, t1));
t1 = Z3_mk_zero_ext(c, 1, t1);
Z3_inc_ref(c, t1);
t2 = Z3_mk_zero_ext(c, 1, t2);
Z3_inc_ref(c, t2);
Z3_ast r = Z3_mk_bvadd(c, t1, t2);
return Z3_mk_eq(c, Z3_mk_extract(c, sz, sz, r), Z3_mk_int(c, 0, Z3_mk_bv_sort(c, 1)));
Z3_inc_ref(c, r);
Z3_ast ex = Z3_mk_extract(c, sz, sz, r);
Z3_inc_ref(c, ex);
Z3_ast result = Z3_mk_eq(c, ex, Z3_mk_int(c, 0, Z3_mk_bv_sort(c, 1)));
Z3_dec_ref(c, t1);
Z3_dec_ref(c, t2);
Z3_dec_ref(c, ex);
Z3_dec_ref(c, r);
return result;
}
Z3_CATCH_RETURN(0);
}
@ -197,10 +237,26 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_TRY;
RESET_ERROR_CODE();
Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1));
Z3_inc_ref(c, zero);
Z3_ast r = Z3_mk_bvadd(c, t1, t2);
Z3_ast args[2] = { Z3_mk_bvslt(c, t1, zero), Z3_mk_bvslt(c, t2, zero) };
Z3_inc_ref(c, r);
Z3_ast l1 = Z3_mk_bvslt(c, t1, zero);
Z3_inc_ref(c, l1);
Z3_ast l2 = Z3_mk_bvslt(c, t2, zero);
Z3_inc_ref(c, l2);
Z3_ast args[2] = { l1, l2 };
Z3_ast args_neg = Z3_mk_and(c, 2, args);
return Z3_mk_implies(c, args_neg, Z3_mk_bvslt(c, r, zero));
Z3_inc_ref(c, args_neg);
Z3_ast lt = Z3_mk_bvslt(c, r, zero);
Z3_inc_ref(c, lt);
Z3_ast result = Z3_mk_implies(c, args_neg, lt);
Z3_dec_ref(c, lt);
Z3_dec_ref(c, l1);
Z3_dec_ref(c, l2);
Z3_dec_ref(c, r);
Z3_dec_ref(c, args_neg);
Z3_dec_ref(c, zero);
return result;
Z3_CATCH_RETURN(0);
}
@ -208,12 +264,28 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2) {
Z3_TRY;
RESET_ERROR_CODE();
Z3_sort s = Z3_get_sort(c, t2);
Z3_ast minus_t2 = Z3_mk_bvneg(c, t2);
Z3_inc_ref(c, minus_t2);
Z3_sort s = Z3_get_sort(c, t2);
Z3_ast min = Z3_mk_bvsmin(c, s);
return Z3_mk_ite(c, Z3_mk_eq(c, t2, min),
Z3_mk_bvslt(c, t1, Z3_mk_int(c, 0, s)),
Z3_mk_bvadd_no_overflow(c, t1, minus_t2, true));
Z3_inc_ref(c, min);
Z3_ast x = Z3_mk_eq(c, t2, min);
Z3_inc_ref(c, x);
Z3_ast zero = Z3_mk_int(c, 0, s);
Z3_inc_ref(c, zero);
Z3_ast y = Z3_mk_bvslt(c, t1, zero);
Z3_inc_ref(c, y);
Z3_ast z = Z3_mk_bvadd_no_overflow(c, t1, minus_t2, true);
Z3_inc_ref(c, z);
Z3_ast result = Z3_mk_ite(c, x, y, z);
mk_c(c)->save_ast_trail(to_app(result));
Z3_dec_ref(c, minus_t2);
Z3_dec_ref(c, min);
Z3_dec_ref(c, x);
Z3_dec_ref(c, y);
Z3_dec_ref(c, z);
Z3_dec_ref(c, zero);
return result;
Z3_CATCH_RETURN(0);
}
@ -222,10 +294,19 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
RESET_ERROR_CODE();
if (is_signed) {
Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1));
if (Z3_get_error_code(c) != Z3_OK) return 0;
Z3_inc_ref(c, zero);
Z3_ast minus_t2 = Z3_mk_bvneg(c, t2);
if (Z3_get_error_code(c) != Z3_OK) return 0;
return Z3_mk_implies(c, Z3_mk_bvslt(c, zero, t2), Z3_mk_bvadd_no_underflow(c, t1, minus_t2));
Z3_inc_ref(c, minus_t2);
Z3_ast x = Z3_mk_bvslt(c, zero, t2);
Z3_inc_ref(c, x);
Z3_ast y = Z3_mk_bvadd_no_underflow(c, t1, minus_t2);
Z3_inc_ref(c, y);
Z3_ast result = Z3_mk_implies(c, x, y);
Z3_dec_ref(c, zero);
Z3_dec_ref(c, minus_t2);
Z3_dec_ref(c, x);
Z3_dec_ref(c, y);
return result;
}
else {
return Z3_mk_bvule(c, t2, t1);
@ -267,12 +348,24 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_TRY;
RESET_ERROR_CODE();
Z3_sort s = Z3_get_sort(c, t1);
if (Z3_get_error_code(c) != Z3_OK) return 0;
Z3_ast min = Z3_mk_bvmsb(c, s);
if (Z3_get_error_code(c) != Z3_OK) return 0;
Z3_ast args[2] = { Z3_mk_eq(c, t1, min),
Z3_mk_eq(c, t2, Z3_mk_int(c, -1, s)) };
return Z3_mk_not(c, Z3_mk_and(c, 2, args));
Z3_inc_ref(c, min);
Z3_ast x = Z3_mk_eq(c, t1, min);
Z3_inc_ref(c, x);
Z3_ast y = Z3_mk_int(c, -1, s);
Z3_inc_ref(c, y);
Z3_ast z = Z3_mk_eq(c, t2, y);
Z3_inc_ref(c, z);
Z3_ast args[2] = { x, z };
Z3_ast u = Z3_mk_and(c, 2, args);
Z3_inc_ref(c, u);
Z3_ast result = Z3_mk_not(c, u);
Z3_dec_ref(c, min);
Z3_dec_ref(c, x);
Z3_dec_ref(c, y);
Z3_dec_ref(c, z);
Z3_dec_ref(c, u);
return result;
Z3_CATCH_RETURN(0);
}

17
src/api/api_util.h
View file

@ -29,7 +29,6 @@ Revision History:
#define Z3_CATCH_RETURN_NO_HANDLE(VAL) } catch (z3_exception &) { return VAL; }
#define CHECK_REF_COUNT(a) (reinterpret_cast<ast const*>(a)->get_ref_count() > 0)
#define VALIDATE(a) SASSERT(!a || CHECK_REF_COUNT(a))
namespace api {
// Generic wrapper for ref-count objects exposed by the API
@ -44,30 +43,30 @@ namespace api {
};
};
inline ast * to_ast(Z3_ast a) { VALIDATE(a); return reinterpret_cast<ast *>(a); }
inline ast * to_ast(Z3_ast a) { return reinterpret_cast<ast *>(a); }
inline Z3_ast of_ast(ast* a) { return reinterpret_cast<Z3_ast>(a); }
inline expr * to_expr(Z3_ast a) { VALIDATE(a); return reinterpret_cast<expr*>(a); }
inline expr * to_expr(Z3_ast a) { return reinterpret_cast<expr*>(a); }
inline Z3_ast of_expr(expr* e) { return reinterpret_cast<Z3_ast>(e); }
inline expr * const * to_exprs(Z3_ast const* a) { return reinterpret_cast<expr* const*>(a); }
inline Z3_ast * const * of_exprs(expr* const* e) { return reinterpret_cast<Z3_ast* const*>(e); }
inline app * to_app(Z3_app a) { VALIDATE(a); return reinterpret_cast<app*>(a); }
inline app * to_app(Z3_ast a) { VALIDATE(a); return reinterpret_cast<app*>(a); }
inline app * to_app(Z3_app a) { return reinterpret_cast<app*>(a); }
inline app * to_app(Z3_ast a) { return reinterpret_cast<app*>(a); }
inline Z3_app of_app(app* a) { return reinterpret_cast<Z3_app>(a); }
inline app * const* to_apps(Z3_ast const* a) { VALIDATE(a); return reinterpret_cast<app * const*>(a); }
inline app * const* to_apps(Z3_ast const* a) { return reinterpret_cast<app * const*>(a); }
inline ast * const * to_asts(Z3_ast const* a) { return reinterpret_cast<ast* const*>(a); }
inline sort * to_sort(Z3_sort a) { VALIDATE(a); return reinterpret_cast<sort*>(a); }
inline sort * to_sort(Z3_sort a) { return reinterpret_cast<sort*>(a); }
inline Z3_sort of_sort(sort* s) { return reinterpret_cast<Z3_sort>(s); }
inline sort * const * to_sorts(Z3_sort const* a) { return reinterpret_cast<sort* const*>(a); }
inline Z3_sort const * of_sorts(sort* const* s) { return reinterpret_cast<Z3_sort const*>(s); }
inline func_decl * to_func_decl(Z3_func_decl a) { VALIDATE(a); return reinterpret_cast<func_decl*>(a); }
inline func_decl * to_func_decl(Z3_func_decl a) { return reinterpret_cast<func_decl*>(a); }
inline Z3_func_decl of_func_decl(func_decl* f) { return reinterpret_cast<Z3_func_decl>(f); }
inline func_decl * const * to_func_decls(Z3_func_decl const* f) { return reinterpret_cast<func_decl*const*>(f); }
@ -75,7 +74,7 @@ inline func_decl * const * to_func_decls(Z3_func_decl const* f) { return reinter
inline symbol to_symbol(Z3_symbol s) { return symbol::mk_symbol_from_c_ptr(reinterpret_cast<void*>(s)); }
inline Z3_symbol of_symbol(symbol s) { return reinterpret_cast<Z3_symbol>(const_cast<void*>(s.c_ptr())); }
inline Z3_pattern of_pattern(ast* a) { VALIDATE(a); return reinterpret_cast<Z3_pattern>(a); }
inline Z3_pattern of_pattern(ast* a) { return reinterpret_cast<Z3_pattern>(a); }
inline app* to_pattern(Z3_pattern p) { return reinterpret_cast<app*>(p); }
inline Z3_lbool of_lbool(lbool b) { return static_cast<Z3_lbool>(b); }

143
src/api/c++/z3++.h
View file

@ -249,6 +249,8 @@ namespace z3 {
array & operator=(array const & s);
public:
array(unsigned sz):m_size(sz) { m_array = new T[sz]; }
template<typename T2>
array(ast_vector_tpl<T2> const & v);
~array() { delete[] m_array; }
unsigned size() const { return m_size; }
T & operator[](int i) { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
@ -872,7 +874,18 @@ namespace z3 {
\brief Return a simplified version of this expression. The parameter \c p is a set of parameters for the Z3 simplifier.
*/
expr simplify(params const & p) const { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
};
/**
\brief Apply substitution. Replace src expressions by dst.
*/
expr substitute(expr_vector const& src, expr_vector const& dst);
/**
\brief Apply substitution. Replace bound variables by expressions.
*/
expr substitute(expr_vector const& dst);
};
/**
\brief Wraps a Z3_ast as an expr object. It also checks for errors.
@ -928,49 +941,6 @@ namespace z3 {
inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); }
inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
// Basic functions for creating quantified formulas.
// The C API should be used for creating quantifiers with patterns, weights, many variables, etc.
inline expr forall(expr const & x, expr const & b) {
check_context(x, b);
Z3_app vars[] = {(Z3_app) x};
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr forall(expr const & x1, expr const & x2, expr const & b) {
check_context(x1, b); check_context(x2, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x3, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr exists(expr const & x, expr const & b) {
check_context(x, b);
Z3_app vars[] = {(Z3_app) x};
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr exists(expr const & x1, expr const & x2, expr const & b) {
check_context(x1, b); check_context(x2, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x3, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
template<typename T> class cast_ast;
template<> class cast_ast<ast> {
@ -1032,6 +1002,67 @@ namespace z3 {
friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
};
template<typename T>
template<typename T2>
array<T>::array(ast_vector_tpl<T2> const & v) {
m_array = new T[v.size()];
m_size = v.size();
for (unsigned i = 0; i < m_size; i++) {
m_array[i] = v[i];
}
}
// Basic functions for creating quantified formulas.
// The C API should be used for creating quantifiers with patterns, weights, many variables, etc.
inline expr forall(expr const & x, expr const & b) {
check_context(x, b);
Z3_app vars[] = {(Z3_app) x};
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr forall(expr const & x1, expr const & x2, expr const & b) {
check_context(x1, b); check_context(x2, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x3, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr forall(expr_vector const & xs, expr const & b) {
array<Z3_app> vars(xs);
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr exists(expr const & x, expr const & b) {
check_context(x, b);
Z3_app vars[] = {(Z3_app) x};
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr exists(expr const & x1, expr const & x2, expr const & b) {
check_context(x1, b); check_context(x2, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x3, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr exists(expr_vector const & xs, expr const & b) {
array<Z3_app> vars(xs);
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
class func_entry : public object {
Z3_func_entry m_entry;
void init(Z3_func_entry e) {
@ -1680,6 +1711,30 @@ namespace z3 {
d.check_error();
return expr(d.ctx(), r);
}
inline expr expr::substitute(expr_vector const& src, expr_vector const& dst) {
assert(src.size() == dst.size());
array<Z3_ast> _src(src.size());
array<Z3_ast> _dst(dst.size());
for (unsigned i = 0; i < src.size(); ++i) {
_src[i] = src[i];
_dst[i] = dst[i];
}
Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
check_error();
return expr(ctx(), r);
}
inline expr expr::substitute(expr_vector const& dst) {
array<Z3_ast> _dst(dst.size());
for (unsigned i = 0; i < dst.size(); ++i) {
_dst[i] = dst[i];
}
Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
check_error();
return expr(ctx(), r);
}
};

15
src/api/dotnet/Context.cs
View file

@ -44,6 +44,21 @@ namespace Microsoft.Z3
/// <summary>
/// Constructor.
/// </summary>
/// <remarks>
/// The following parameters can be set:
/// - proof (Boolean) Enable proof generation
/// - debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting
/// - trace (Boolean) Tracing support for VCC
/// - trace_file_name (String) Trace out file for VCC traces
/// - timeout (unsigned) default timeout (in milliseconds) used for solvers
/// - well_sorted_check type checker
/// - auto_config use heuristics to automatically select solver and configure it
/// - model model generation for solvers, this parameter can be overwritten when creating a solver
/// - model_validate validate models produced by solvers
/// - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver
/// Note that in previous versions of Z3, this constructor was also used to set global and module parameters.
/// For this purpose we should now use <see cref="Global.SetParameter"/>
/// </remarks>
public Context(Dictionary<string, string> settings)
: base()
{

2
src/api/dotnet/Microsoft.Z3.csproj
View file

@ -399,4 +399,4 @@
<Target Name="AfterBuild">
</Target>
-->
</Project>
</Project>

15
src/api/java/Context.java
View file

@ -27,6 +27,21 @@ public class Context extends IDisposable
/**
* Constructor.
* <remarks>
* The following parameters can be set:
* - proof (Boolean) Enable proof generation
* - debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting
* - trace (Boolean) Tracing support for VCC
* - trace_file_name (String) Trace out file for VCC traces
* - timeout (unsigned) default timeout (in milliseconds) used for solvers
* - well_sorted_check type checker
* - auto_config use heuristics to automatically select solver and configure it
* - model model generation for solvers, this parameter can be overwritten when creating a solver
* - model_validate validate models produced by solvers
* - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver
* Note that in previous versions of Z3, this constructor was also used to set global and
* module parameters. For this purpose we should now use <see cref="Global.setParameter"/>
* </remarks>
**/
public Context(Map<String, String> settings) throws Z3Exception
{

46
src/api/ml/README-test-win
View file

@ -1,23 +1,23 @@
This directory contains scripts to build the test application using
OCaml. You also need CamlIDL to be able to generate the OCaml API.
- To download OCaml:
http://caml.inria.fr/ocaml/
- To download CamlIDL:
http://forge.ocamlcore.org/projects/camlidl/
- One must build the OCaml library before compiling the example.
Go to directory ../ocaml
- Use 'build-test.cmd' to build the test application using the OCaml compiler.
Remark: The OCaml and C compiler tool chains must be configured in your environment.
Running from the Visual Studio Command Prompt configures the Microsoft C compiler.
- The script 'exec.cmd' adds the bin directory to the path. So,
test_mlapi.exe can find z3.dll.
This directory contains scripts to build the test application using
OCaml. You also need CamlIDL to be able to generate the OCaml API.
- To download OCaml:
http://caml.inria.fr/ocaml/
- To download CamlIDL:
http://forge.ocamlcore.org/projects/camlidl/
- One must build the OCaml library before compiling the example.
Go to directory ../ocaml
- Use 'build-test.cmd' to build the test application using the OCaml compiler.
Remark: The OCaml and C compiler tool chains must be configured in your environment.
Running from the Visual Studio Command Prompt configures the Microsoft C compiler.
- The script 'exec.cmd' adds the bin directory to the path. So,
test_mlapi.exe can find z3.dll.

46
src/api/ml/README-win
View file

@ -1,23 +1,23 @@
The OCaml API for Z3 was tested using OCaml 3.12.1.
You also need CamlIDL to be able to generate the OCaml API.
- To download OCaml:
http://caml.inria.fr/ocaml/
- To download CamlIDL:
http://forge.ocamlcore.org/projects/camlidl/
- To build the OCaml API for Z3:
.\build-lib.cmd
Remark: The OCaml and C compiler tool chains must be configured in your environment.
Running from the Visual Studio Command Prompt configures the Microsoft C compiler.
Remark: Building the OCaml API copies some pathnames into files,
so the OCaml API must be recompiled if the Z3 library files are moved.
See ..\examples\ocaml\build-test.cmd for an example of how to compile and link with Z3.
Acknowledgements:
The OCaml interface for Z3 was written by Josh Berdine and Jakob Lichtenberg.
Many thanks to them!
The OCaml API for Z3 was tested using OCaml 3.12.1.
You also need CamlIDL to be able to generate the OCaml API.
- To download OCaml:
http://caml.inria.fr/ocaml/
- To download CamlIDL:
http://forge.ocamlcore.org/projects/camlidl/
- To build the OCaml API for Z3:
.\build-lib.cmd
Remark: The OCaml and C compiler tool chains must be configured in your environment.
Running from the Visual Studio Command Prompt configures the Microsoft C compiler.
Remark: Building the OCaml API copies some pathnames into files,
so the OCaml API must be recompiled if the Z3 library files are moved.
See ..\examples\ocaml\build-test.cmd for an example of how to compile and link with Z3.
Acknowledgements:
The OCaml interface for Z3 was written by Josh Berdine and Jakob Lichtenberg.
Many thanks to them!

6
src/api/ml/build-lib.cmd
View file

@ -1,3 +1,3 @@
@echo off
call .\compile_mlapi.cmd ..\include ..\bin ..\bin
@echo off
call .\compile_mlapi.cmd ..\include ..\bin ..\bin

38
src/api/ml/build-test.cmd
View file

@ -1,19 +1,19 @@
@echo off
if not exist ..\..\ocaml\z3.cmxa (
echo "YOU MUST BUILD OCAML API! Go to directory ..\ocaml"
goto :EOF
)
REM ocaml (>= 3.11) calls the linker through flexlink
ocamlc -version >> ocaml_version
set /p OCAML_VERSION= <ocaml_version
if %OCAML_VERSION% GEQ 3.11 (
set XCFLAGS=
) else (
set XCFLAGS=/nologo /MT /DWIN32
)
ocamlc -w A -ccopt "%XCFLAGS%" -o test_mlapi_byte.exe -I ..\..\ocaml z3.cma test_mlapi.ml
ocamlopt -w A -ccopt "%XCFLAGS%" -o test_mlapi.exe -I ..\..\ocaml z3.cmxa test_mlapi.ml
@echo off
if not exist ..\..\ocaml\z3.cmxa (
echo "YOU MUST BUILD OCAML API! Go to directory ..\ocaml"
goto :EOF
)
REM ocaml (>= 3.11) calls the linker through flexlink
ocamlc -version >> ocaml_version
set /p OCAML_VERSION= <ocaml_version
if %OCAML_VERSION% GEQ 3.11 (
set XCFLAGS=
) else (
set XCFLAGS=/nologo /MT /DWIN32
)
ocamlc -w A -ccopt "%XCFLAGS%" -o test_mlapi_byte.exe -I ..\..\ocaml z3.cma test_mlapi.ml
ocamlopt -w A -ccopt "%XCFLAGS%" -o test_mlapi.exe -I ..\..\ocaml z3.cmxa test_mlapi.ml

10
src/api/ml/exec.cmd
View file

@ -1,5 +1,5 @@
@echo off
SETLOCAL
set PATH=..\..\bin;%PATH%
test_mlapi.exe
ENDLOCAL
@echo off
SETLOCAL
set PATH=..\..\bin;%PATH%
test_mlapi.exe
ENDLOCAL

3
src/api/python/z3.py
View file

@ -585,6 +585,9 @@ class FuncDeclRef(AstRef):
def as_ast(self):
return Z3_func_decl_to_ast(self.ctx_ref(), self.ast)
def as_func_decl(self):
return self.ast
def name(self):
"""Return the name of the function declaration `self`.