diff --git a/scripts/update_api.py b/scripts/update_api.py index 791c23ddd..09c4fbe1c 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -123,7 +123,6 @@ SYMBOL = 9 PRINT_MODE = 10 ERROR_CODE = 11 DOUBLE = 12 -UINT_PTR = 13 FIRST_OBJ_ID = 100 @@ -132,28 +131,28 @@ def is_obj(ty): Type2Str = { VOID : 'void', VOID_PTR : 'void*', INT : 'int', UINT : 'unsigned', INT64 : '__int64', UINT64 : '__uint64', DOUBLE : 'double', STRING : 'Z3_string', STRING_PTR : 'Z3_string_ptr', BOOL : 'Z3_bool', SYMBOL : 'Z3_symbol', - PRINT_MODE : 'Z3_ast_print_mode', ERROR_CODE : 'Z3_error_code', UINT_PTR : 'unsigned*' + PRINT_MODE : 'Z3_ast_print_mode', ERROR_CODE : 'Z3_error_code' } Type2PyStr = { VOID_PTR : 'ctypes.c_void_p', INT : 'ctypes.c_int', UINT : 'ctypes.c_uint', INT64 : 'ctypes.c_longlong', UINT64 : 'ctypes.c_ulonglong', DOUBLE : 'ctypes.c_double', STRING : 'ctypes.c_char_p', STRING_PTR : 'ctypes.POINTER(ctypes.c_char_p)', BOOL : 'ctypes.c_bool', SYMBOL : 'Symbol', - PRINT_MODE : 'ctypes.c_uint', ERROR_CODE : 'ctypes.c_uint', UINT_PTR : 'ctypes.POINTER(ctypes.c_uint)' + PRINT_MODE : 'ctypes.c_uint', ERROR_CODE : 'ctypes.c_uint' } # Mapping to .NET types Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', INT64 : 'Int64', UINT64 : 'UInt64', DOUBLE : 'double', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'int', SYMBOL : 'IntPtr', - PRINT_MODE : 'uint', ERROR_CODE : 'uint', UINT_PTR : 'uint[]'} + PRINT_MODE : 'uint', ERROR_CODE : 'uint' } # Mapping to Java types Type2Java = { VOID : 'void', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double', STRING : 'String', STRING_PTR : 'StringPtr', - BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int', UINT_PTR : 'int[]'} + BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int'} Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', INT64 : 'jlong', UINT64 : 'jlong', DOUBLE : 'jdouble', STRING : 'jstring', STRING_PTR : 'jobject', - BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint', UINT_PTR : 'jlong'} + BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint'} next_type_id = FIRST_OBJ_ID @@ -964,7 +963,6 @@ def def_API(name, result, params): tstr = type2str(ty) if sz_p_k == OUT or sz_p_k == INOUT: sz_e = ("(*a%s)" % sz) - tstr = tstr + '*' else: sz_e = ("a%s" % sz) log_c.write(" for (unsigned i = 0; i < %s; i++) { " % sz_e) @@ -978,11 +976,6 @@ def def_API(name, result, params): log_c.write(" }\n") log_c.write(" Au(%s);\n" % sz_e) exe_c.write("in.get_uint_array(%s)" % i) - elif ty == UINT_PTR: - log_c.write("P(0);") - log_c.write(" }\n") - log_c.write(" Ap(%s);\n" % sz_e) - exe_c.write("reinterpret_cast<%s>(in.get_obj_array(%s))" % (tstr, i)) else: error ("unsupported parameter for %s, %s" % (name, p)) else: diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 0bfb2d077..3e9ddc8a3 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -123,89 +123,6 @@ extern "C" { } } - Z3_lbool Z3_interpolate(Z3_context ctx, - unsigned num, - Z3_ast *cnsts, - unsigned *parents, - Z3_params options, - Z3_ast *interps, - Z3_model *model, - Z3_literals *labels, - unsigned incremental, - unsigned num_theory, - Z3_ast *theory - ){ - - - profiling::timer_start("Solve"); - - if (!incremental){ - - profiling::timer_start("Z3 assert"); - - Z3_push(ctx); // so we can rewind later - - for (unsigned i = 0; i < num; i++) - Z3_assert_cnstr(ctx, cnsts[i]); // assert all the constraints - - if (theory){ - for (unsigned i = 0; i < num_theory; i++) - Z3_assert_cnstr(ctx, theory[i]); - } - - profiling::timer_stop("Z3 assert"); - } - - - // Get a proof of unsat - - Z3_ast proof; - Z3_lbool result; - - profiling::timer_start("Z3 solving"); - result = Z3_check_assumptions(ctx, 0, 0, model, &proof, 0, 0); - profiling::timer_stop("Z3 solving"); - - switch (result) { - case Z3_L_FALSE: - - Z3_interpolate_proof(ctx, - proof, - num, - cnsts, - parents, - options, - interps, - num_theory, - theory); - - if (!incremental) - for (unsigned i = 0; i < num - 1; i++) - Z3_persist_ast(ctx, interps[i], 1); - break; - - case Z3_L_UNDEF: - if (labels) - *labels = Z3_get_relevant_labels(ctx); - break; - - case Z3_L_TRUE: - if (labels) - *labels = Z3_get_relevant_labels(ctx); - break; - } - - profiling::timer_start("Z3 pop"); - if (!incremental) - Z3_pop(ctx, 1); - profiling::timer_stop("Z3 pop"); - - profiling::timer_stop("Solve"); - - return result; - - } - static std::ostringstream itp_err; int Z3_check_interpolant(Z3_context ctx, @@ -603,7 +520,7 @@ extern "C" { } - int Z3_read_interpolation_problem(Z3_context ctx, unsigned *_num, Z3_ast **cnsts, unsigned **parents, const char *filename, const char **error, unsigned *ret_num_theory, Z3_ast **theory){ + int Z3_read_interpolation_problem(Z3_context ctx, unsigned *_num, Z3_ast cnsts[], unsigned parents[], const char *filename, Z3_string_ptr error, unsigned *ret_num_theory, Z3_ast theory[]){ hash_map file_params; get_file_params(filename, file_params); @@ -632,11 +549,11 @@ extern "C" { if (ret_num_theory) *ret_num_theory = num_theory; if (theory) - *theory = &read_theory[0]; + theory = &read_theory[0]; if (!parents){ *_num = num; - *cnsts = &read_cnsts[0]; + cnsts = &read_cnsts[0]; return true; } @@ -706,8 +623,8 @@ extern "C" { } *_num = num; - *cnsts = &read_cnsts[0]; - *parents = &read_parents[0]; + cnsts = &read_cnsts[0]; + parents = &read_parents[0]; return true; fail: @@ -717,3 +634,87 @@ extern "C" { } } + + +#if 0 +/** Constant reprepresenting a root of a formula tree for tree interpolation */ +#define IZ3_ROOT SHRT_MAX + +/** This function uses Z3 to determine satisfiability of a set of +constraints. If UNSAT, an interpolant is returned, based on the +refutation generated by Z3. If SAT, a model is returned. + +If "parents" is non-null, computes a tree interpolant. The tree is +defined by the array "parents". This array maps each formula in +the tree to its parent, where formulas are indicated by their +integer index in "cnsts". The parent of formula n must have index +greater than n. The last formula is the root of the tree. Its +parent entry should be the constant IZ3_ROOT. + +If "parents" is null, computes a sequence interpolant. + +\param ctx The Z3 context. Must be generated by iz3_mk_context +\param num The number of constraints in the sequence +\param cnsts Array of constraints (AST's in context ctx) +\param parents The parents vector defining the tree structure +\param options Interpolation options (may be NULL) +\param interps Array to return interpolants (size at least num-1, may be NULL) +\param model Returns a Z3 model if constraints SAT (may be NULL) +\param labels Returns relevant labels if SAT (may be NULL) +\param incremental + +VERY IMPORTANT: All the Z3 formulas in cnsts must be in Z3 +context ctx. The model and interpolants returned are also +in this context. + +The return code is as in Z3_check_assumptions, that is, + +Z3_L_FALSE = constraints UNSAT (interpolants returned) +Z3_L_TRUE = constraints SAT (model returned) +Z3_L_UNDEF = Z3 produced no result, or interpolation not possible + +Currently, this function supports integer and boolean variables, +as well as arrays over these types, with linear arithmetic, +uninterpreted functions and quantifiers over integers (that is +AUFLIA). Interpolants are produced in AULIA. However, some +uses of array operations may cause quantifiers to appear in the +interpolants even when there are no quantifiers in the input formulas. +Although quantifiers may appear in the input formulas, Z3 may give up in +this case, returning Z3_L_UNDEF. + +If "incremental" is true, cnsts must contain exactly the set of +formulas that are currently asserted in the context. If false, +there must be no formulas currently asserted in the context. +Setting "incremental" to true makes it posisble to incrementally +add and remove constraints from the context until the context +becomes UNSAT, at which point an interpolant is computed. Caution +must be used, however. Before popping the context, if you wish to +keep the interolant formulas, you *must* preserve them by using +Z3_persist_ast. Also, if you want to simplify the interpolant +formulas using Z3_simplify, you must first pop all of the +assertions in the context (or use a different context). Otherwise, +the formulas will be simplified *relative* to these constraints, +which is almost certainly not what you want. + + +Current limitations on tree interpolants. In a tree interpolation +problem, each constant (0-ary function symbol) must occur only +along one path from root to leaf. Function symbols (of arity > 0) +are considered to have global scope (i.e., may appear in any +interpolant formula). + +def_API('Z3_interpolate', BOOL, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in(PARAMS), _out_array(1, AST), _out(MODEL), _out(LITERALS), _in(UINT), _in(UINT), _in_array(9, AST))) +*/ + +Z3_lbool Z3_API Z3_interpolate(__in Z3_context ctx, + __in unsigned num, + __in_ecount(num) Z3_ast *cnsts, + __in_ecount(num) unsigned *parents, + __in Z3_params options, + __out_ecount(num - 1) Z3_ast *interps, + __out Z3_model *model, + __out Z3_literals *labels, + __in unsigned incremental, + __in unsigned num_theory, + __in_ecount(num_theory) Z3_ast *theory); +#endif \ No newline at end of file diff --git a/src/api/dotnet/InterpolationContext.cs b/src/api/dotnet/InterpolationContext.cs index 559a1bfc7..fbedadffe 100644 --- a/src/api/dotnet/InterpolationContext.cs +++ b/src/api/dotnet/InterpolationContext.cs @@ -89,47 +89,6 @@ namespace Microsoft.Z3 return (Z3_lbool)r; } - /// - /// Computes an interpolant. - /// - /// For more information on interpolation please refer - /// too the function Z3_compute_interpolant in the C/C++ API, which is - /// well documented. - Z3_lbool Interpolate(Expr[] cnsts, uint[] parents, Params options, bool incremental, Expr[] theory, out Expr[] interps, out Model model) - { - Contract.Requires(cnsts != null); - Contract.Requires(parents != null); - Contract.Requires(cnsts.Length == parents.Length); - Contract.Ensures(Contract.ValueAtReturn(out interps) != null); - Contract.Ensures(Contract.ValueAtReturn(out model) != null); - - CheckContextMatch(cnsts); - CheckContextMatch(theory); - - uint sz = (uint)cnsts.Length; - - IntPtr[] ni = new IntPtr[sz - 1]; - IntPtr nm = IntPtr.Zero; - IntPtr z = IntPtr.Zero; - - int r = Native.Z3_interpolate(nCtx, - sz, Expr.ArrayToNative(cnsts), parents, - options.NativeObject, - out ni, - ref nm, - ref z, // Z3_lterals are deprecated. - (uint)(incremental ? 1 : 0), - (uint)theory.Length, Expr.ArrayToNative(theory)); - - interps = new Expr[sz - 1]; - for (uint i = 0; i < sz - 1; i++) - interps[i] = Expr.Create(this, ni[i]); - - model = new Model(this, nm); - - return (Z3_lbool)r; - } - /// /// Return a string summarizing cumulative time used for interpolation. /// @@ -150,7 +109,7 @@ namespace Microsoft.Z3 public int CheckInterpolant(Expr[] cnsts, uint[] parents, Expr[] interps, out string error, Expr[] theory) { Contract.Requires(cnsts.Length == parents.Length); - Contract.Requires(cnsts.Length == interps.Length+1); + Contract.Requires(cnsts.Length == interps.Length + 1); IntPtr n_err_str; int r = Native.Z3_check_interpolant(nCtx, (uint)cnsts.Length, @@ -170,25 +129,27 @@ namespace Microsoft.Z3 /// For more information on interpolation please refer /// too the function Z3_read_interpolation_problem in the C/C++ API, which is /// well documented. - public int ReadInterpolationProblem(string filename, out Expr[] cnsts, out uint[] parents, out string error, out Expr[] theory) + public int ReadInterpolationProblem(string filename, out Expr[] cnsts, ref uint[] parents, out string error, out Expr[] theory) { uint num = 0, num_theory = 0; - IntPtr[] n_cnsts; - IntPtr[] n_theory; + IntPtr n_cnsts = new IntPtr(); + IntPtr n_theory = new IntPtr(); IntPtr n_err_str; - uint[][] n_parents; - int r = Native.Z3_read_interpolation_problem(nCtx, ref num, out n_cnsts, out n_parents, filename, out n_err_str, ref num_theory, out n_theory); + int r = Native.Z3_read_interpolation_problem(nCtx, ref num, ref n_cnsts, out parents, filename, out n_err_str, ref num_theory, ref n_theory); error = Marshal.PtrToStringAnsi(n_err_str); cnsts = new Expr[num]; parents = new uint[num]; - theory = new Expr[num_theory]; + theory = new Expr[num_theory]; for (int i = 0; i < num; i++) { - cnsts[i] = Expr.Create(this, n_cnsts[i]); - parents[i] = n_parents[0][i]; + IntPtr ce = new IntPtr(n_cnsts.ToInt64() + (IntPtr.Size * i)); + cnsts[i] = Expr.Create(this, ce); } for (int i = 0; i < num_theory; i++) - theory[i] = Expr.Create(this, n_theory[i]); + { + IntPtr te = new IntPtr(n_theory.ToInt64() + (IntPtr.Size * i)); + theory[i] = Expr.Create(this, te); + } return r; } @@ -198,9 +159,10 @@ namespace Microsoft.Z3 /// For more information on interpolation please refer /// too the function Z3_write_interpolation_problem in the C/C++ API, which is /// well documented. - public void WriteInterpolationProblem(string filename, Expr[] cnsts, int[] parents, string error, Expr[] theory) + public void WriteInterpolationProblem(string filename, Expr[] cnsts, uint[] parents, string error, Expr[] theory) { Contract.Requires(cnsts.Length == parents.Length); + Native.Z3_write_interpolation_problem(nCtx, (uint)cnsts.Length, Expr.ArrayToNative(cnsts), parents, error, (uint)theory.Length, Expr.ArrayToNative(theory)); } } } diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 41ccf532e..04e2d38af 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1779,7 +1779,7 @@ extern "C" { Z3_sort Z3_API Z3_mk_tuple_sort(__in Z3_context c, __in Z3_symbol mk_tuple_name, __in unsigned num_fields, - __in_ecount(num_fields) Z3_symbol const field_names[], + __in_ecount(num_fields) Z3_symbol const field_names[], __in_ecount(num_fields) Z3_sort const field_sorts[], __out Z3_func_decl * mk_tuple_decl, __out_ecount(num_fields) Z3_func_decl proj_decl[]); @@ -4907,8 +4907,7 @@ END_MLAPI_EXCLUDE __in_ecount(num_sorts) Z3_sort const sorts[], __in unsigned num_decls, __in_ecount(num_decls) Z3_symbol const decl_names[], - __in_ecount(num_decls) Z3_func_decl const decls[] - ); + __in_ecount(num_decls) Z3_func_decl const decls[]); /** \brief Similar to #Z3_parse_smtlib2_string, but reads the benchmark from a file. @@ -4917,13 +4916,12 @@ END_MLAPI_EXCLUDE */ Z3_ast Z3_API Z3_parse_smtlib2_file(__in Z3_context c, __in Z3_string file_name, - __in unsigned num_sorts, - __in_ecount(num_sorts) Z3_symbol const sort_names[], - __in_ecount(num_sorts) Z3_sort const sorts[], - __in unsigned num_decls, - __in_ecount(num_decls) Z3_symbol const decl_names[], - __in_ecount(num_decls) Z3_func_decl const decls[] - ); + __in unsigned num_sorts, + __in_ecount(num_sorts) Z3_symbol const sort_names[], + __in_ecount(num_sorts) Z3_sort const sorts[], + __in unsigned num_decls, + __in_ecount(num_decls) Z3_symbol const decl_names[], + __in_ecount(num_decls) Z3_func_decl const decls[]); #ifdef ML4only #include diff --git a/src/api/z3_interp.h b/src/api/z3_interp.h index 1aac13b6e..88ba83e2d 100644 --- a/src/api/z3_interp.h +++ b/src/api/z3_interp.h @@ -163,88 +163,6 @@ extern "C" { __out Z3_ast_vector *interp, __out Z3_model *model); - - /** Constant reprepresenting a root of a formula tree for tree interpolation */ -#define IZ3_ROOT SHRT_MAX - - /** This function uses Z3 to determine satisfiability of a set of - constraints. If UNSAT, an interpolant is returned, based on the - refutation generated by Z3. If SAT, a model is returned. - - If "parents" is non-null, computes a tree interpolant. The tree is - defined by the array "parents". This array maps each formula in - the tree to its parent, where formulas are indicated by their - integer index in "cnsts". The parent of formula n must have index - greater than n. The last formula is the root of the tree. Its - parent entry should be the constant IZ3_ROOT. - - If "parents" is null, computes a sequence interpolant. - - \param ctx The Z3 context. Must be generated by iz3_mk_context - \param num The number of constraints in the sequence - \param cnsts Array of constraints (AST's in context ctx) - \param parents The parents vector defining the tree structure - \param options Interpolation options (may be NULL) - \param interps Array to return interpolants (size at least num-1, may be NULL) - \param model Returns a Z3 model if constraints SAT (may be NULL) - \param labels Returns relevant labels if SAT (may be NULL) - \param incremental - - VERY IMPORTANT: All the Z3 formulas in cnsts must be in Z3 - context ctx. The model and interpolants returned are also - in this context. - - The return code is as in Z3_check_assumptions, that is, - - Z3_L_FALSE = constraints UNSAT (interpolants returned) - Z3_L_TRUE = constraints SAT (model returned) - Z3_L_UNDEF = Z3 produced no result, or interpolation not possible - - Currently, this function supports integer and boolean variables, - as well as arrays over these types, with linear arithmetic, - uninterpreted functions and quantifiers over integers (that is - AUFLIA). Interpolants are produced in AULIA. However, some - uses of array operations may cause quantifiers to appear in the - interpolants even when there are no quantifiers in the input formulas. - Although quantifiers may appear in the input formulas, Z3 may give up in - this case, returning Z3_L_UNDEF. - - If "incremental" is true, cnsts must contain exactly the set of - formulas that are currently asserted in the context. If false, - there must be no formulas currently asserted in the context. - Setting "incremental" to true makes it posisble to incrementally - add and remove constraints from the context until the context - becomes UNSAT, at which point an interpolant is computed. Caution - must be used, however. Before popping the context, if you wish to - keep the interolant formulas, you *must* preserve them by using - Z3_persist_ast. Also, if you want to simplify the interpolant - formulas using Z3_simplify, you must first pop all of the - assertions in the context (or use a different context). Otherwise, - the formulas will be simplified *relative* to these constraints, - which is almost certainly not what you want. - - - Current limitations on tree interpolants. In a tree interpolation - problem, each constant (0-ary function symbol) must occur only - along one path from root to leaf. Function symbols (of arity > 0) - are considered to have global scope (i.e., may appear in any - interpolant formula). - - def_API('Z3_interpolate', BOOL, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in(PARAMS), _out_array(1, AST), _out(MODEL), _out(LITERALS), _in(UINT), _in(UINT), _in_array(9, AST))) - */ - - Z3_lbool Z3_API Z3_interpolate(__in Z3_context ctx, - __in unsigned num, - __in_ecount(num) Z3_ast *cnsts, - __in_ecount(num) unsigned *parents, - __in Z3_params options, - __out_ecount(num - 1) Z3_ast *interps, - __out Z3_model *model, - __out Z3_literals *labels, - __in unsigned incremental, - __in unsigned num_theory, - __in_ecount(num_theory) Z3_ast *theory); - /** Return a string summarizing cumulative time used for interpolation. This string is purely for entertainment purposes and has no semantics. @@ -288,18 +206,18 @@ extern "C" { where each value is represented using the common symbols between the formulas in the subtree and the remainder of the formulas. - def_API('Z3_read_interpolation_problem', INT, (_in(CONTEXT), _out(UINT), _out_array(1, AST), _out_array(1, UINT_PTR), _in(STRING), _out(STRING), _out(UINT), _out_array(6, AST))) + def_API('Z3_read_interpolation_problem', INT, (_in(CONTEXT), _out(UINT), _out(AST), _out_array(1, UINT), _in(STRING), _out(STRING), _out(UINT), _out(AST))) */ int Z3_API Z3_read_interpolation_problem(__in Z3_context ctx, __out unsigned *num, - __out_ecount(*num) Z3_ast **cnsts, - __out_ecount(*num) unsigned **parents, + __out Z3_ast *cnsts, + __out unsigned parents[], __in Z3_string filename, - __out Z3_string *error, + __out_opt Z3_string_ptr error, __out unsigned *num_theory, - __out_ecount(*num_theory) Z3_ast **theory); + __out Z3_ast theory[]); @@ -323,12 +241,12 @@ extern "C" { int Z3_API Z3_check_interpolant(__in Z3_context ctx, __in unsigned num, - __in_ecount(num) Z3_ast *cnsts, - __in_ecount(num) unsigned *parents, + __in_ecount(num) Z3_ast cnsts[], + __in_ecount(num) unsigned parents[], __in_ecount(num - 1) Z3_ast *interps, - __out Z3_string *error, + __out_opt Z3_string_ptr error, __in unsigned num_theory, - __in_ecount(num_theory) Z3_ast *theory); + __in_ecount(num_theory) Z3_ast theory[]); /** Write an interpolation problem to file suitable for reading with Z3_read_interpolation_problem. The output file is a sequence @@ -346,11 +264,11 @@ extern "C" { void Z3_API Z3_write_interpolation_problem(__in Z3_context ctx, __in unsigned num, - __in_ecount(num) Z3_ast *cnsts, - __in_ecount(num) unsigned *parents, + __in_ecount(num) Z3_ast cnsts[], + __in_ecount(num) unsigned parents[], __in Z3_string filename, __in unsigned num_theory, - __in_ecount(num_theory) Z3_ast *theory); + __in_ecount(num_theory) Z3_ast theory[]); #ifdef __cplusplus };