mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-11-06 10:03:03 -08:00
commit 6f8ff46ddb
259 changed files with 5223 additions and 3243 deletions
Download patch file Download diff file Expand all files Collapse all files

88
src/api/api_array.cpp
View file

@ -34,6 +34,19 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const* domain, Z3_sort range) {
Z3_TRY;
LOG_Z3_mk_array_sort_n(c, n, domain, range);
RESET_ERROR_CODE();
vector<parameter> params;
for (unsigned i = 0; i < n; ++i) params.push_back(parameter(to_sort(domain[i])));
params.push_back(parameter(to_sort(range)));
sort * ty = mk_c(c)->m().mk_sort(mk_c(c)->get_array_fid(), ARRAY_SORT, params.size(), params.c_ptr());
mk_c(c)->save_ast_trail(ty);
RETURN_Z3(of_sort(ty));
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i) {
Z3_TRY;
LOG_Z3_mk_select(c, a, i);
@ -57,6 +70,35 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_select_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const* idxs) {
Z3_TRY;
LOG_Z3_mk_select_n(c, a, n, idxs);
RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m();
expr * _a = to_expr(a);
// expr * _i = to_expr(i);
sort * a_ty = m.get_sort(_a);
// sort * i_ty = m.get_sort(_i);
if (a_ty->get_family_id() != mk_c(c)->get_array_fid()) {
SET_ERROR_CODE(Z3_SORT_ERROR);
RETURN_Z3(0);
}
ptr_vector<sort> domain;
ptr_vector<expr> args;
args.push_back(_a);
domain.push_back(a_ty);
for (unsigned i = 0; i < n; ++i) {
args.push_back(to_expr(idxs[i]));
domain.push_back(m.get_sort(to_expr(idxs[i])));
}
func_decl * d = m.mk_func_decl(mk_c(c)->get_array_fid(), OP_SELECT, 2, a_ty->get_parameters(), domain.size(), domain.c_ptr());
app * r = m.mk_app(d, args.size(), args.c_ptr());
mk_c(c)->save_ast_trail(r);
check_sorts(c, r);
RETURN_Z3(of_ast(r));
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v) {
Z3_TRY;
LOG_Z3_mk_store(c, a, i, v);
@ -82,6 +124,37 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const* idxs, Z3_ast v) {
Z3_TRY;
LOG_Z3_mk_store_n(c, a, n, idxs, v);
RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m();
expr * _a = to_expr(a);
expr * _v = to_expr(v);
sort * a_ty = m.get_sort(_a);
sort * v_ty = m.get_sort(_v);
if (a_ty->get_family_id() != mk_c(c)->get_array_fid()) {
SET_ERROR_CODE(Z3_SORT_ERROR);
RETURN_Z3(0);
}
ptr_vector<sort> domain;
ptr_vector<expr> args;
args.push_back(_a);
domain.push_back(a_ty);
for (unsigned i = 0; i < n; ++i) {
args.push_back(to_expr(idxs[i]));
domain.push_back(m.get_sort(to_expr(idxs[i])));
}
args.push_back(_v);
domain.push_back(v_ty);
func_decl * d = m.mk_func_decl(mk_c(c)->get_array_fid(), OP_STORE, 2, a_ty->get_parameters(), domain.size(), domain.c_ptr());
app * r = m.mk_app(d, args.size(), args.c_ptr());
mk_c(c)->save_ast_trail(r);
check_sorts(c, r);
RETURN_Z3(of_ast(r));
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const* args) {
Z3_TRY;
LOG_Z3_mk_map(c, f, n, args);
@ -188,6 +261,18 @@ extern "C" {
MK_BINARY(Z3_mk_set_subset, mk_c(c)->get_array_fid(), OP_SET_SUBSET, SKIP);
MK_BINARY(Z3_mk_array_ext, mk_c(c)->get_array_fid(), OP_ARRAY_EXT, SKIP);
Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f) {
Z3_TRY;
LOG_Z3_mk_as_array(c, f);
RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m();
array_util a(m);
app * r = a.mk_as_array(to_func_decl(f));
mk_c(c)->save_ast_trail(r);
return of_ast(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set) {
return Z3_mk_select(c, set, elem);
}
@ -222,7 +307,8 @@ extern "C" {
CHECK_VALID_AST(t, 0);
if (to_sort(t)->get_family_id() == mk_c(c)->get_array_fid() &&
to_sort(t)->get_decl_kind() == ARRAY_SORT) {
Z3_sort r = reinterpret_cast<Z3_sort>(to_sort(t)->get_parameter(1).get_ast());
unsigned n = to_sort(t)->get_num_parameters();
Z3_sort r = reinterpret_cast<Z3_sort>(to_sort(t)->get_parameter(n-1).get_ast());
RETURN_Z3(r);
}
SET_ERROR_CODE(Z3_INVALID_ARG);

2
src/api/api_interp.cpp
View file

@ -249,7 +249,7 @@ extern "C" {
params_ref _p;
_p.set_bool("proof", true); // this is currently useless
scoped_proof_mode spm(mk_c(c)->m(), PGM_FINE);
scoped_proof_mode spm(mk_c(c)->m(), PGM_ENABLED);
scoped_ptr<solver_factory> sf = mk_smt_solver_factory();
scoped_ptr<solver> m_solver((*sf)(mk_c(c)->m(), _p, true, true, true, ::symbol::null));
m_solver.get()->updt_params(_p); // why do we have to do this?

9
src/api/api_model.cpp
View file

@ -255,8 +255,13 @@ extern "C" {
LOG_Z3_add_const_interp(c, m, f, a);
RESET_ERROR_CODE();
func_decl* d = to_func_decl(f);
model* mdl = to_model_ref(m);
mdl->register_decl(d, to_expr(a));
if (d->get_arity() != 0) {
SET_ERROR_CODE(Z3_INVALID_ARG);
}
else {
model* mdl = to_model_ref(m);
mdl->register_decl(d, to_expr(a));
}
Z3_CATCH;
}

16
src/api/api_opt.cpp
View file

@ -288,15 +288,16 @@ extern "C" {
Z3_optimize opt,
std::istream& s) {
ast_manager& m = mk_c(c)->m();
cmd_context ctx(false, &m);
install_opt_cmds(ctx, to_optimize_ptr(opt));
ctx.set_ignore_check(true);
if (!parse_smt2_commands(ctx, s)) {
scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &m);
install_opt_cmds(*ctx.get(), to_optimize_ptr(opt));
ctx->set_ignore_check(true);
if (!parse_smt2_commands(*ctx.get(), s)) {
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR);
return;
}
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
ptr_vector<expr>::const_iterator it = ctx->begin_assertions();
ptr_vector<expr>::const_iterator end = ctx->end_assertions();
for (; it != end; ++it) {
to_optimize_ptr(opt)->add_hard_constraint(*it);
}
@ -325,9 +326,6 @@ extern "C" {
std::ostringstream strm;
strm << "Could not open file " << s;
throw default_exception(strm.str());
SET_ERROR_CODE(Z3_PARSER_ERROR);
return;
}
Z3_optimize_from_stream(c, d, is);
Z3_CATCH;

28
src/api/api_parsers.cpp
View file

@ -57,7 +57,7 @@ extern "C" {
Z3_func_decl const decls[]) {
Z3_TRY;
LOG_Z3_parse_smtlib_string(c, str, num_sorts, sort_names, sorts, num_decls, decl_names, decls);
std::ostringstream* outs = alloc(std::ostringstream);
scoped_ptr<std::ostringstream> outs = alloc(std::ostringstream);
bool ok = false;
RESET_ERROR_CODE();
@ -70,7 +70,7 @@ extern "C" {
ok = false;
}
mk_c(c)->m_smtlib_error_buffer = outs->str();
dealloc(outs);
outs = nullptr;
if (!ok) {
mk_c(c)->reset_parser();
SET_ERROR_CODE(Z3_PARSER_ERROR);
@ -90,7 +90,7 @@ extern "C" {
LOG_Z3_parse_smtlib_file(c, file_name, num_sorts, sort_names, types, num_decls, decl_names, decls);
bool ok = false;
RESET_ERROR_CODE();
std::ostringstream* outs = alloc(std::ostringstream);
scoped_ptr<std::ostringstream> outs = alloc(std::ostringstream);
init_smtlib_parser(c, num_sorts, sort_names, types, num_decls, decl_names, decls);
mk_c(c)->m_smtlib_parser->set_error_stream(*outs);
try {
@ -100,7 +100,7 @@ extern "C" {
ok = false;
}
mk_c(c)->m_smtlib_error_buffer = outs->str();
dealloc(outs);
outs = nullptr;
if (!ok) {
mk_c(c)->reset_parser();
SET_ERROR_CODE(Z3_PARSER_ERROR);
@ -263,24 +263,24 @@ extern "C" {
Z3_symbol const decl_names[],
Z3_func_decl const decls[]) {
Z3_TRY;
cmd_context ctx(false, &(mk_c(c)->m()));
ctx.set_ignore_check(true);
scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &(mk_c(c)->m()));
ctx->set_ignore_check(true);
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
mk_c(c)->save_object(v);
mk_c(c)->save_object(v);
for (unsigned i = 0; i < num_decls; ++i) {
ctx.insert(to_symbol(decl_names[i]), to_func_decl(decls[i]));
ctx->insert(to_symbol(decl_names[i]), to_func_decl(decls[i]));
}
for (unsigned i = 0; i < num_sorts; ++i) {
psort* ps = ctx.pm().mk_psort_cnst(to_sort(sorts[i]));
ctx.insert(ctx.pm().mk_psort_user_decl(0, to_symbol(sort_names[i]), ps));
psort* ps = ctx->pm().mk_psort_cnst(to_sort(sorts[i]));
ctx->insert(ctx->pm().mk_psort_user_decl(0, to_symbol(sort_names[i]), ps));
}
if (!parse_smt2_commands(ctx, is)) {
if (!parse_smt2_commands(*ctx.get(), is)) {
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR);
return of_ast_vector(v);
}
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
ptr_vector<expr>::const_iterator it = ctx->begin_assertions();
ptr_vector<expr>::const_iterator end = ctx->end_assertions();
for (; it != end; ++it) {
v->m_ast_vector.push_back(*it);
}

4
src/api/api_quant.cpp
View file

@ -63,9 +63,11 @@ extern "C" {
RESET_ERROR_CODE();
if (!mk_c(c)->m().is_bool(to_expr(body))) {
SET_ERROR_CODE(Z3_SORT_ERROR);
return nullptr;
}
if (num_patterns > 0 && num_no_patterns > 0) {
SET_ERROR_CODE(Z3_INVALID_USAGE);
return nullptr;
}
expr * const* ps = reinterpret_cast<expr * const*>(patterns);
expr * const* no_ps = reinterpret_cast<expr * const*>(no_patterns);
@ -76,7 +78,7 @@ extern "C" {
for (unsigned i = 0; i < num_patterns; i++) {
if (!v(num_decls, ps[i], 0, 0)) {
SET_ERROR_CODE(Z3_INVALID_PATTERN);
return 0;
return nullptr;
}
}
}

94
src/api/api_solver.cpp
View file

@ -33,6 +33,9 @@ Revision History:
#include "smt/smt_solver.h"
#include "smt/smt_implied_equalities.h"
#include "solver/smt_logics.h"
#include "cmd_context/cmd_context.h"
#include "parsers/smt2/smt2parser.h"
extern "C" {
@ -121,6 +124,30 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name) {
Z3_TRY;
LOG_Z3_solver_from_file(c, s, file_name);
scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &(mk_c(c)->m()));
ctx->set_ignore_check(true);
std::ifstream is(file_name);
if (!is) {
SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR);
return;
}
if (!parse_smt2_commands(*ctx.get(), is)) {
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR);
return;
}
ptr_vector<expr>::const_iterator it = ctx->begin_assertions();
ptr_vector<expr>::const_iterator end = ctx->end_assertions();
for (; it != end; ++it) {
to_solver_ref(s)->assert_expr(*it);
}
to_solver_ref(s)->set_model_converter(ctx->get_model_converter());
Z3_CATCH;
}
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s) {
Z3_TRY;
LOG_Z3_solver_get_help(c, s);
@ -452,6 +479,7 @@ extern "C" {
unsigned sz = __assumptions.size();
for (unsigned i = 0; i < sz; ++i) {
if (!is_expr(__assumptions[i])) {
_assumptions.finalize(); _consequences.finalize(); _variables.finalize();
SET_ERROR_CODE(Z3_INVALID_USAGE);
return Z3_L_UNDEF;
}
@ -461,6 +489,7 @@ extern "C" {
sz = __variables.size();
for (unsigned i = 0; i < sz; ++i) {
if (!is_expr(__variables[i])) {
_assumptions.finalize(); _consequences.finalize(); _variables.finalize();
SET_ERROR_CODE(Z3_INVALID_USAGE);
return Z3_L_UNDEF;
}
@ -481,6 +510,7 @@ extern "C" {
}
catch (z3_exception & ex) {
to_solver_ref(s)->set_reason_unknown(eh);
_assumptions.finalize(); _consequences.finalize(); _variables.finalize();
mk_c(c)->handle_exception(ex);
return Z3_L_UNDEF;
}
@ -522,69 +552,5 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_solver_lookahead(Z3_context c,
Z3_solver s,
Z3_ast_vector assumptions,
Z3_ast_vector candidates) {
Z3_TRY;
LOG_Z3_solver_lookahead(c, s, assumptions, candidates);
ast_manager& m = mk_c(c)->m();
expr_ref_vector _candidates(m), _assumptions(m);
ast_ref_vector const& __candidates = to_ast_vector_ref(candidates);
ast_ref_vector const& __assumptions = to_ast_vector_ref(assumptions);
for (auto & e : __candidates) {
if (!is_expr(e)) {
SET_ERROR_CODE(Z3_INVALID_USAGE);
return 0;
}
_candidates.push_back(to_expr(e));
}
for (auto & e : __assumptions) {
if (!is_expr(e)) {
SET_ERROR_CODE(Z3_INVALID_USAGE);
return 0;
}
_assumptions.push_back(to_expr(e));
}
expr_ref result(m);
unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
unsigned rlimit = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", false);
cancel_eh<reslimit> eh(mk_c(c)->m().limit());
api::context::set_interruptable si(*(mk_c(c)), eh);
{
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
scoped_timer timer(timeout, &eh);
scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
try {
result = to_solver_ref(s)->lookahead(_assumptions, _candidates);
}
catch (z3_exception & ex) {
mk_c(c)->handle_exception(ex);
return 0;
}
}
mk_c(c)->save_ast_trail(result);
RETURN_Z3(of_ast(result));
Z3_CATCH_RETURN(0);
}
Z3_ast_vector Z3_API Z3_solver_get_lemmas(Z3_context c, Z3_solver s) {
Z3_TRY;
LOG_Z3_solver_get_lemmas(c, s);
RESET_ERROR_CODE();
ast_manager& m = mk_c(c)->m();
init_solver(c, s);
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
mk_c(c)->save_object(v);
expr_ref_vector lemmas(m);
to_solver_ref(s)->get_lemmas(lemmas);
for (expr* e : lemmas) {
v->m_ast_vector.push_back(e);
}
RETURN_Z3(of_ast_vector(v));
Z3_CATCH_RETURN(0);
}
};

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

@ -140,18 +140,17 @@ namespace z3 {
class context {
bool m_enable_exceptions;
Z3_context m_ctx;
static void Z3_API error_handler(Z3_context /*c*/, Z3_error_code /*e*/) { /* do nothing */ }
void init(config & c) {
m_ctx = Z3_mk_context_rc(c);
m_enable_exceptions = true;
Z3_set_error_handler(m_ctx, error_handler);
Z3_set_error_handler(m_ctx, 0);
Z3_set_ast_print_mode(m_ctx, Z3_PRINT_SMTLIB2_COMPLIANT);
}
void init_interp(config & c) {
m_ctx = Z3_mk_interpolation_context(c);
m_enable_exceptions = true;
Z3_set_error_handler(m_ctx, error_handler);
Z3_set_error_handler(m_ctx, 0);
Z3_set_ast_print_mode(m_ctx, Z3_PRINT_SMTLIB2_COMPLIANT);
}
@ -251,6 +250,8 @@ namespace z3 {
Example: Given a context \c c, <tt>c.array_sort(c.int_sort(), c.bool_sort())</tt> is an array sort from integer to Boolean.
*/
sort array_sort(sort d, sort r);
sort array_sort(sort_vector const& d, sort r);
/**
\brief Return an enumeration sort: enum_names[0], ..., enum_names[n-1].
\c cs and \c ts are output parameters. The method stores in \c cs the constants corresponding to the enumerated elements,
@ -2328,6 +2329,11 @@ namespace z3 {
inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
inline sort context::array_sort(sort d, sort r) { Z3_sort s = Z3_mk_array_sort(m_ctx, d, r); check_error(); return sort(*this, s); }
inline sort context::array_sort(sort_vector const& d, sort r) {
array<Z3_sort> dom(d);
Z3_sort s = Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error(); return sort(*this, s);
}
inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
array<Z3_symbol> _enum_names(n);
for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
@ -2574,11 +2580,32 @@ namespace z3 {
a.check_error();
return expr(a.ctx(), r);
}
inline expr select(expr const & a, expr_vector const & i) {
check_context(a, i);
array<Z3_ast> idxs(i);
Z3_ast r = Z3_mk_select_n(a.ctx(), a, idxs.size(), idxs.ptr());
a.check_error();
return expr(a.ctx(), r);
}
inline expr store(expr const & a, int i, expr const & v) { return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), v); }
inline expr store(expr const & a, expr i, int v) { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
inline expr store(expr const & a, int i, int v) {
return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
}
inline expr store(expr const & a, expr_vector const & i, expr const & v) {
check_context(a, i); check_context(a, v);
array<Z3_ast> idxs(i);
Z3_ast r = Z3_mk_store_n(a.ctx(), a, idxs.size(), idxs.ptr(), v);
a.check_error();
return expr(a.ctx(), r);
}
inline expr as_array(func_decl & f) {
Z3_ast r = Z3_mk_as_array(f.ctx(), f);
f.check_error();
return expr(f.ctx(), r);
}
#define MK_EXPR1(_fn, _arg) \
Z3_ast r = _fn(_arg.ctx(), _arg); \

7
src/api/dotnet/ArraySort.cs
View file

@ -63,6 +63,13 @@ namespace Microsoft.Z3
Contract.Requires(domain != null);
Contract.Requires(range != null);
}
internal ArraySort(Context ctx, Sort[] domain, Sort range)
: base(ctx, Native.Z3_mk_array_sort_n(ctx.nCtx, (uint)domain.Length, AST.ArrayToNative(domain), range.NativeObject))
{
Contract.Requires(ctx != null);
Contract.Requires(domain != null);
Contract.Requires(range != null);
}
#endregion
};

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

@ -274,6 +274,20 @@ namespace Microsoft.Z3
return new ArraySort(this, domain, range);
}
/// <summary>
/// Create a new n-ary array sort.
/// </summary>
public ArraySort MkArraySort(Sort[] domain, Sort range)
{
Contract.Requires(domain != null);
Contract.Requires(range != null);
Contract.Ensures(Contract.Result<ArraySort>() != null);
CheckContextMatch<Sort>(domain);
CheckContextMatch(range);
return new ArraySort(this, domain, range);
}
/// <summary>
/// Create a new tuple sort.
/// </summary>
@ -2113,6 +2127,7 @@ namespace Microsoft.Z3
return (ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range));
}
/// <summary>
/// Array read.
/// </summary>
@ -2123,8 +2138,8 @@ namespace Microsoft.Z3
/// The node <c>a</c> must have an array sort <c>[domain -> range]</c>,
/// and <c>i</c> must have the sort <c>domain</c>.
/// The sort of the result is <c>range</c>.
/// <seealso cref="MkArraySort"/>
/// <seealso cref="MkStore"/>
/// <seealso cref="MkArraySort(Sort, Sort)"/>
/// <seealso cref="MkStore(ArrayExpr, Expr, Expr)"/>
/// </remarks>
public Expr MkSelect(ArrayExpr a, Expr i)
{
@ -2137,6 +2152,30 @@ namespace Microsoft.Z3
return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
}
/// <summary>
/// Array read.
/// </summary>
/// <remarks>
/// The argument <c>a</c> is the array and <c>args</c> are the indices
/// of the array that gets read.
///
/// The node <c>a</c> must have an array sort <c>[domain1,..,domaink -> range]</c>,
/// and <c>args</c> must have the sort <c>domain1,..,domaink</c>.
/// The sort of the result is <c>range</c>.
/// <seealso cref="MkArraySort(Sort, Sort)"/>
/// <seealso cref="MkStore(ArrayExpr, Expr, Expr)"/>
/// </remarks>
public Expr MkSelect(ArrayExpr a, params Expr[] args)
{
Contract.Requires(a != null);
Contract.Requires(args != null && Contract.ForAll(args, n => n != null));
Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(a);
CheckContextMatch<Expr>(args);
return Expr.Create(this, Native.Z3_mk_select_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
}
/// <summary>
/// Array update.
/// </summary>
@ -2151,8 +2190,9 @@ namespace Microsoft.Z3
/// on all indices except for <c>i</c>, where it maps to <c>v</c>
/// (and the <c>select</c> of <c>a</c> with
/// respect to <c>i</c> may be a different value).
/// <seealso cref="MkArraySort"/>
/// <seealso cref="MkSelect"/>
/// <seealso cref="MkArraySort(Sort, Sort)"/>
/// <seealso cref="MkSelect(ArrayExpr, Expr)"/>
/// <seealso cref="MkSelect(ArrayExpr, Expr[])"/>
/// </remarks>
public ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v)
{
@ -2167,14 +2207,45 @@ namespace Microsoft.Z3
return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
}
/// <summary>
/// Array update.
/// </summary>
/// <remarks>
/// The node <c>a</c> must have an array sort <c>[domain1,..,domaink -> range]</c>,
/// <c>args</c> must have sort <c>domain1,..,domaink</c>,
/// <c>v</c> must have sort range. The sort of the result is <c>[domain -> range]</c>.
/// The semantics of this function is given by the theory of arrays described in the SMT-LIB
/// standard. See http://smtlib.org for more details.
/// The result of this function is an array that is equal to <c>a</c>
/// (with respect to <c>select</c>)
/// on all indices except for <c>args</c>, where it maps to <c>v</c>
/// (and the <c>select</c> of <c>a</c> with
/// respect to <c>args</c> may be a different value).
/// <seealso cref="MkArraySort(Sort, Sort)"/>
/// <seealso cref="MkSelect(ArrayExpr, Expr)"/>
/// <seealso cref="MkSelect(ArrayExpr, Expr[])"/>
/// </remarks>
public ArrayExpr MkStore(ArrayExpr a, Expr[] args, Expr v)
{
Contract.Requires(a != null);
Contract.Requires(args != null);
Contract.Requires(v != null);
Contract.Ensures(Contract.Result<ArrayExpr>() != null);
CheckContextMatch<Expr>(args);
CheckContextMatch(a);
CheckContextMatch(v);
return new ArrayExpr(this, Native.Z3_mk_store_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args), v.NativeObject));
}
/// <summary>
/// Create a constant array.
/// </summary>
/// <remarks>
/// The resulting term is an array, such that a <c>select</c>on an arbitrary index
/// produces the value <c>v</c>.
/// <seealso cref="MkArraySort"/>
/// <seealso cref="MkSelect"/>
/// <seealso cref="MkArraySort(Sort, Sort)"/>
/// <seealso cref="MkSelect(ArrayExpr, Expr)"/>
/// </remarks>
public ArrayExpr MkConstArray(Sort domain, Expr v)
{
@ -2194,9 +2265,9 @@ namespace Microsoft.Z3
/// Eeach element of <c>args</c> must be of an array sort <c>[domain_i -> range_i]</c>.
/// The function declaration <c>f</c> must have type <c> range_1 .. range_n -> range</c>.
/// <c>v</c> must have sort range. The sort of the result is <c>[domain_i -> range]</c>.
/// <seealso cref="MkArraySort"/>
/// <seealso cref="MkSelect"/>
/// <seealso cref="MkStore"/>
/// <seealso cref="MkArraySort(Sort, Sort)"/>
/// <seealso cref="MkSelect(ArrayExpr, Expr)"/>
/// <seealso cref="MkStore(ArrayExpr, Expr, Expr)"/>
/// </remarks>
public ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
{

55
src/api/dotnet/Solver.cs
View file

@ -181,6 +181,14 @@ namespace Microsoft.Z3
Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject);
}
/// <summary>
/// Load solver assertions from a file.
/// </summary>
public void FromFile(string file)
{
Native.Z3_solver_from_file(Context.nCtx, NativeObject, file);
}
/// <summary>
/// Assert a lemma (or multiple) into the solver.
/// </summary>
@ -275,31 +283,6 @@ namespace Microsoft.Z3
return lboolToStatus(r);
}
/// <summary>
/// Select a lookahead literal from the set of supplied candidates.
/// </summary>
public BoolExpr Lookahead(IEnumerable<BoolExpr> assumptions, IEnumerable<BoolExpr> candidates)
{
ASTVector cands = new ASTVector(Context);
foreach (var c in candidates) cands.Push(c);
ASTVector assums = new ASTVector(Context);
foreach (var c in assumptions) assums.Push(c);
return (BoolExpr)Expr.Create(Context, Native.Z3_solver_lookahead(Context.nCtx, NativeObject, assums.NativeObject, cands.NativeObject));
}
/// <summary>
/// Retrieve set of lemmas that have been inferred by solver.
/// </summary>
public BoolExpr[] Lemmas
{
get
{
var r = Native.Z3_solver_get_lemmas(Context.nCtx, NativeObject);
var v = new ASTVector(Context, r);
return v.ToBoolExprArray();
}
}
/// <summary>
/// The model of the last <c>Check</c>.
/// </summary>
@ -370,6 +353,28 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Return a set of cubes.
/// </summary>
public IEnumerable<BoolExpr> Cube()
{
int rounds = 0;
while (true) {
BoolExpr r = (BoolExpr)Expr.Create(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject));
if (r.IsFalse) {
if (rounds == 0)
yield return r;
break;
}
if (r.IsTrue) {
yield return r;
break;
}
++rounds;
yield return r;
}
}
/// <summary>
/// Create a clone of the current solver with respect to <c>ctx</c>.
/// </summary>

6
src/api/java/ArraySort.java
View file

@ -56,4 +56,10 @@ public class ArraySort extends Sort
super(ctx, Native.mkArraySort(ctx.nCtx(), domain.getNativeObject(),
range.getNativeObject()));
}
ArraySort(Context ctx, Sort[] domains, Sort range)
{
super(ctx, Native.mkArraySortN(ctx.nCtx(), domains.length, AST.arrayToNative(domains),
range.getNativeObject()));
}
};

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

@ -224,6 +224,17 @@ public class Context implements AutoCloseable {
return new ArraySort(this, domain, range);
}
/**
* Create a new array sort.
**/
public ArraySort mkArraySort(Sort[] domains, Sort range)
{
checkContextMatch(domains);
checkContextMatch(range);
return new ArraySort(this, domains, range);
}
/**
* Create a new string sort
**/
@ -414,7 +425,7 @@ public class Context implements AutoCloseable {
* that is passed in as argument is updated with value v,
* the remaining fields of t are unchanged.
**/
public Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
public Expr mkUpdateField(FuncDecl field, Expr t, Expr v)
throws Z3Exception
{
return Expr.create (this,
@ -706,7 +717,7 @@ public class Context implements AutoCloseable {
}
/**
* Mk an expression representing {@code not(a)}.
* Create an expression representing {@code not(a)}.
**/
public BoolExpr mkNot(BoolExpr a)
{
@ -1679,6 +1690,28 @@ public class Context implements AutoCloseable {
i.getNativeObject()));
}
/**
* Array read.
* Remarks: The argument {@code a} is the array and
* {@code args} are the indices of the array that gets read.
*
* The node {@code a} must have an array sort
* {@code [domains -> range]}, and {@code args} must have the sorts
* {@code domains}. The sort of the result is {@code range}.
*
* @see #mkArraySort
* @see #mkStore
**/
public Expr mkSelect(ArrayExpr a, Expr[] args)
{
checkContextMatch(a);
checkContextMatch(args);
return Expr.create(
this,
Native.mkSelectN(nCtx(), a.getNativeObject(), args.length, AST.arrayToNative(args)));
}
/**
* Array update.
* Remarks: The node {@code a} must have an array sort
@ -1704,6 +1737,31 @@ public class Context implements AutoCloseable {
i.getNativeObject(), v.getNativeObject()));
}
/**
* Array update.
* Remarks: The node {@code a} must have an array sort
* {@code [domains -> range]}, {@code i} must have sort
* {@code domain}, {@code v} must have sort range. The sort of the
* result is {@code [domains -> range]}. The semantics of this function
* is given by the theory of arrays described in the SMT-LIB standard. See
* http://smtlib.org for more details. The result of this function is an
* array that is equal to {@code a} (with respect to
* {@code select}) on all indices except for {@code args}, where it
* maps to {@code v} (and the {@code select} of {@code a}
* with respect to {@code args} may be a different value).
* @see #mkArraySort
* @see #mkSelect
**/
public ArrayExpr mkStore(ArrayExpr a, Expr[] args, Expr v)
{
checkContextMatch(a);
checkContextMatch(args);
checkContextMatch(v);
return new ArrayExpr(this, Native.mkStoreN(nCtx(), a.getNativeObject(),
args.length, AST.arrayToNative(args), v.getNativeObject()));
}
/**
* Create a constant array.
* Remarks: The resulting term is an array, such
@ -2104,7 +2162,7 @@ public class Context implements AutoCloseable {
/**
* Create a range expression.
*/
public ReExpr MkRange(SeqExpr lo, SeqExpr hi)
public ReExpr mkRange(SeqExpr lo, SeqExpr hi)
{
checkContextMatch(lo, hi);
return (ReExpr) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));

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

@ -6279,21 +6279,6 @@ class Solver(Z3PPObject):
consequences = [ consequences[i] for i in range(sz) ]
return CheckSatResult(r), consequences
def lemmas(self):
"""Extract auxiliary lemmas produced by solver"""
return AstVector(Z3_solver_get_lemmas(self.ctx.ref(), self.solver), self.ctx)
def lookahead(self, candidates = None):
"""Get lookahead literal"""
if candidates is None:
candidates = AstVector(None, self.ctx)
elif not isinstance(candidates, AstVector):
_cs = AstVector(None, self.ctx)
for c in candidates:
_asms.push(c)
candidates = _cs
return _to_expr_ref(Z3_solver_lookahead(self.ctx.ref(), self.solver, candidates), self.ctx)
def cube(self):
"""Get set of cubes"""
rounds = 0
@ -6315,11 +6300,11 @@ class Solver(Z3PPObject):
def from_file(self, filename):
"""Parse assertions from a file"""
self.add([f for f in parse_smt2_file(filename)])
Z3_solver_from_file(self.ctx.ref(), self.solver)
def from_string(self, s):
"""Parse assertions from a string"""
self.add([f for f in parse_smt2_string(s)])
self.add([f for f in parse_smt2_string(s, ctx=self.ctx)])
def assertions(self):
"""Return an AST vector containing all added constraints.

65
src/api/z3_api.h
View file

@ -1881,6 +1881,17 @@ extern "C" {
*/
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range);
/**
\brief Create an array type with N arguments
\sa Z3_mk_select_n
\sa Z3_mk_store_n
def_API('Z3_mk_array_sort_n', SORT, (_in(CONTEXT), _in(UINT), _in_array(1, SORT), _in(SORT)))
*/
Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const * domain, Z3_sort range);
/**
\brief Create a tuple type.
@ -2973,6 +2984,15 @@ extern "C" {
*/
Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i);
/**
\brief n-ary Array read.
The argument \c a is the array and \c idxs are the indices of the array that gets read.
def_API('Z3_mk_select_n', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST)))
*/
Z3_ast Z3_API Z3_mk_select_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const* idxs);
/**
\brief Array update.
@ -2991,6 +3011,14 @@ extern "C" {
*/
Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v);
/**
\brief n-ary Array update.
def_API('Z3_mk_store_n', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const* idxs, Z3_ast v);
/**
\brief Create the constant array.
@ -3031,6 +3059,15 @@ extern "C" {
def_API('Z3_mk_array_default', AST, (_in(CONTEXT), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array);
/**
\brief Create array with the same interpretation as a function.
The array satisfies the property (f x) = (select (_ as-array f) x)
for every argument x.
def_API('Z3_mk_as_array', AST, (_in(CONTEXT), _in(FUNC_DECL)))
*/
Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f);
/*@}*/
/** @name Sets */
@ -3854,6 +3891,7 @@ extern "C" {
/**
\brief Return the domain of the given array sort.
In the case of a multi-dimensional array, this function returns the sort of the first dimension.
\pre Z3_get_sort_kind(c, t) == Z3_ARRAY_SORT
@ -6099,6 +6137,13 @@ extern "C" {
*/
void Z3_API Z3_solver_assert_lemma(Z3_context c, Z3_solver s, Z3_ast a);
/**
\brief load solver assertions from a file.
def_API('Z3_solver_from_file', VOID, (_in(CONTEXT), _in(SOLVER), _in(STRING)))
*/
void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name);
/**
\brief Return the set of asserted formulas on the solver.
@ -6174,14 +6219,6 @@ extern "C" {
Z3_ast_vector variables,
Z3_ast_vector consequences);
/**
\brief select a literal from the list of candidate propositional variables to split on.
If the candidate list is empty, then the solver chooses a formula based on its internal state.
def_API('Z3_solver_lookahead', AST, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR), _in(AST_VECTOR)))
*/
Z3_ast Z3_API Z3_solver_lookahead(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector candidates);
/**
\brief extract a next cube for a solver. The last cube is the constant \c true or \c false.
@ -6193,18 +6230,6 @@ extern "C" {
Z3_ast Z3_API Z3_solver_cube(Z3_context c, Z3_solver s);
/**
\brief retrieve lemmas from solver state. Lemmas are auxiliary unit literals,
binary clauses and other learned clauses that are below a minimal glue level.
Lemmas that have been retrieved in a previous call may be suppressed from subsequent
calls.
def_API('Z3_solver_get_lemmas', AST_VECTOR, (_in(CONTEXT), _in(SOLVER)))
*/
Z3_ast_vector Z3_API Z3_solver_get_lemmas(Z3_context c, Z3_solver s);
/**
\brief Retrieve the model for the last #Z3_solver_check or #Z3_solver_check_assumptions