diff --git a/examples/interp/iz3.cpp b/examples/interp/iz3.cpp index fa7d8b896..6d631ebc9 100755 --- a/examples/interp/iz3.cpp +++ b/examples/interp/iz3.cpp @@ -90,12 +90,12 @@ int main(int argc, const char **argv) { /* Read an interpolation problem */ - int num; + unsigned num; Z3_ast *constraints; - int *parents = 0; + unsigned *parents = 0; const char *error; bool ok; - int num_theory; + unsigned num_theory; Z3_ast *theory; ok = Z3_read_interpolation_problem(ctx, &num, &constraints, tree_mode ? &parents : 0, filename, &error, &num_theory, &theory); @@ -144,7 +144,7 @@ int main(int argc, const char **argv) { if(!incremental_mode){ /* In non-incremental mode, we just pass the constraints. */ - result = Z3_interpolate(ctx, num, constraints, (unsigned int *)parents, options, interpolants, &model, 0, false, num_theory, theory); + result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, constraints, parents, options, interpolants, &model, 0, false, num_theory, theory); } else { @@ -165,7 +165,7 @@ int main(int argc, const char **argv) { for(int i = 0; i < num; i++){ asserted[i] = constraints[i]; Z3_assert_cnstr(ctx,constraints[i]); // assert one constraint - result = Z3_interpolate(ctx, num, &asserted[0], (unsigned int *)parents, options, interpolants, &model, 0, true, 0, 0); + result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, &asserted[0], parents, options, interpolants, &model, 0, true, 0, 0); if(result == Z3_L_FALSE){ for(unsigned j = 0; j < num-1; j++) /* Since we want the interpolant formulas to survive a "pop", we diff --git a/scripts/update_api.py b/scripts/update_api.py index 791c23ddd..837c2e1f4 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -108,6 +108,7 @@ INOUT = 2 IN_ARRAY = 3 OUT_ARRAY = 4 INOUT_ARRAY = 5 +OUT_MANAGED_ARRAY = 6 # Primitive Types VOID = 0 @@ -123,7 +124,6 @@ SYMBOL = 9 PRINT_MODE = 10 ERROR_CODE = 11 DOUBLE = 12 -UINT_PTR = 13 FIRST_OBJ_ID = 100 @@ -132,28 +132,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 @@ -225,6 +225,10 @@ def _out_array2(cap, sz, ty): def _inout_array(sz, ty): return (INOUT_ARRAY, ty, sz, sz); +def _out_managed_array(sz,ty): + return (OUT_MANAGED_ARRAY, ty, 0, sz) + + def param_kind(p): return p[0] @@ -255,11 +259,11 @@ def param2dotnet(p): return "out IntPtr" else: return "[In, Out] ref %s" % type2dotnet(param_type(p)) - if k == IN_ARRAY: + elif k == IN_ARRAY: return "[In] %s[]" % type2dotnet(param_type(p)) - if k == INOUT_ARRAY: + elif k == INOUT_ARRAY: return "[In, Out] %s[]" % type2dotnet(param_type(p)) - if k == OUT_ARRAY: + elif k == OUT_ARRAY or k == OUT_MANAGED_ARRAY: return "[Out] out %s[]" % type2dotnet(param_type(p)) else: return type2dotnet(param_type(p)) @@ -269,7 +273,7 @@ def param2java(p): if k == OUT: if param_type(p) == INT or param_type(p) == UINT: return "IntPtr" - elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) >= FIRST_OBJ_ID: + elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) == VOID_PTR or param_type(p) >= FIRST_OBJ_ID: return "LongPtr" elif param_type(p) == STRING: return "StringPtr" @@ -277,8 +281,13 @@ def param2java(p): print("ERROR: unreachable code") assert(False) exit(1) - if k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: + elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: return "%s[]" % type2java(param_type(p)) + elif k == OUT_MANAGED_ARRAY: + if param_type(p) == UINT: + return "UIntArrayPtr" + else: + return "ObjArrayPtr" else: return type2java(param_type(p)) @@ -467,7 +476,7 @@ def mk_dotnet_wrappers(): dotnet.write('out '); else: dotnet.write('ref ') - elif param_kind(param) == OUT_ARRAY: + elif param_kind(param) == OUT_ARRAY or param_kind(param) == OUT_MANAGED_ARRAY: dotnet.write('out '); dotnet.write('a%d' % i) i = i + 1 @@ -525,6 +534,8 @@ def mk_java(): java_native.write(' public static class IntPtr { public int value; }\n') java_native.write(' public static class LongPtr { public long value; }\n') java_native.write(' public static class StringPtr { public String value; }\n') + java_native.write(' public static class ObjArrayPtr { public long[] value; }\n') + java_native.write(' public static class UIntArrayPtr { public int[] value; }\n') java_native.write(' public static native void setInternalErrorHandler(long ctx);\n\n') if IS_WINDOWS or os.uname()[0]=="CYGWIN": java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name) @@ -679,9 +690,11 @@ def mk_java(): if param_type(param) == INT or param_type(param) == UINT: java_wrapper.write(' jenv->GetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i)) else: - java_wrapper.write(' GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i)) + java_wrapper.write(' GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i)) elif k == IN and param_type(param) == STRING: java_wrapper.write(' Z3_string _a%s = (Z3_string) jenv->GetStringUTFChars(a%s, NULL);\n' % (i, i)) + elif k == OUT_MANAGED_ARRAY: + java_wrapper.write(' %s * _a%s = 0;\n' % (type2str(param_type(param)), i)) i = i + 1 # invoke procedure java_wrapper.write(' ') @@ -700,6 +713,8 @@ def mk_java(): java_wrapper.write('&_a%s' % i) elif k == OUT_ARRAY or k == IN_ARRAY or k == INOUT_ARRAY: java_wrapper.write('_a%s' % i) + elif k == OUT_MANAGED_ARRAY: + java_wrapper.write('&_a%s' % i) elif k == IN and param_type(param) == STRING: java_wrapper.write('_a%s' % i) else: @@ -735,6 +750,8 @@ def mk_java(): java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "J");\n') java_wrapper.write(' jenv->SetLongField(a%s, fid, (jlong) _a%s);\n' % (i, i)) java_wrapper.write(' }\n') + elif k == OUT_MANAGED_ARRAY: + java_wrapper.write(' *(jlong**)a%s = (jlong*)_a%s;\n' % (i, i)) i = i + 1 # return if result == STRING: @@ -935,6 +952,9 @@ def def_API(name, result, params): elif ty == INT64: log_c.write(" I(0);\n") exe_c.write("in.get_int64_addr(%s)" % i) + elif ty == VOID_PTR: + log_c.write(" P(0);\n") + exe_c.write("in.get_obj_addr(%s)" % i) else: error("unsupported parameter for %s, %s" % (name, p)) elif kind == IN_ARRAY or kind == INOUT_ARRAY: @@ -964,7 +984,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,13 +997,22 @@ 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)) + elif kind == OUT_MANAGED_ARRAY: + sz = param_array_size_pos(p) + sz_p = params[sz] + sz_p_k = param_kind(sz_p) + tstr = type2str(ty) + if sz_p_k == OUT or sz_p_k == INOUT: + sz_e = ("(*a%s)" % sz) + else: + sz_e = ("a%s" % sz) + log_c.write(" for (unsigned i = 0; i < %s; i++) { " % sz_e) + 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)) i = i + 1 diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 0bfb2d077..dbf68da38 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); @@ -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/c++/z3++.h b/src/api/c++/z3++.h index 20100d124..c35208d86 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1432,12 +1432,12 @@ namespace z3 { t1.check_error(); return tactic(t1.ctx(), r); } - friend tactic repeat(tactic const & t, unsigned max=UINT_MAX); + friend tactic repeat(tactic const & t, unsigned max); friend tactic with(tactic const & t, params const & p); friend tactic try_for(tactic const & t, unsigned ms); }; - inline tactic repeat(tactic const & t, unsigned max) { + inline tactic repeat(tactic const & t, unsigned max=UINT_MAX) { Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max); t.check_error(); return tactic(t.ctx(), r); diff --git a/src/api/dotnet/InterpolationContext.cs b/src/api/dotnet/InterpolationContext.cs index 559a1bfc7..b5ada1bbd 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, @@ -176,17 +135,13 @@ namespace Microsoft.Z3 IntPtr[] n_cnsts; IntPtr[] n_theory; 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, out n_cnsts, out parents, filename, out n_err_str, ref num_theory, out 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]; - } for (int i = 0; i < num_theory; i++) theory[i] = Expr.Create(this, n_theory[i]); return r; @@ -198,9 +153,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, Expr[] theory) { Contract.Requires(cnsts.Length == parents.Length); + Native.Z3_write_interpolation_problem(nCtx, (uint)cnsts.Length, Expr.ArrayToNative(cnsts), parents, filename, (uint)theory.Length, Expr.ArrayToNative(theory)); } } } diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java new file mode 100644 index 000000000..067871324 --- /dev/null +++ b/src/api/java/InterpolationContext.java @@ -0,0 +1,169 @@ +/** + * + */ +package com.microsoft.z3; + +import java.util.Map; +import java.lang.String; + +import com.microsoft.z3.Native.IntPtr; +import com.microsoft.z3.Native.UIntArrayPtr; +import com.microsoft.z3.enumerations.Z3_lbool; + +/** + * The InterpolationContext is suitable for generation of interpolants. + * + * For more information on interpolation please refer + * too the C/C++ API, which is well documented. + **/ +public class InterpolationContext extends Context +{ + /** + * Constructor. + **/ + public InterpolationContext() throws Z3Exception + { + m_ctx = Native.mkInterpolationContext(0); + initContext(); + } + + /** + * Constructor. + * + * + **/ + public InterpolationContext(Map settings) throws Z3Exception + { + long cfg = Native.mkConfig(); + for (Map.Entry kv : settings.entrySet()) + Native.setParamValue(cfg, kv.getKey(), kv.getValue()); + m_ctx = Native.mkInterpolationContext(cfg); + Native.delConfig(cfg); + initContext(); + } + + /** + * Create an expression that marks a formula position for interpolation. + * @throws Z3Exception + **/ + public BoolExpr MkInterpolant(BoolExpr a) throws Z3Exception + { + checkContextMatch(a); + return new BoolExpr(this, Native.mkInterpolant(nCtx(), a.getNativeObject())); + } + + /** + * Computes an interpolant. + * For more information on interpolation please refer + * too the function Z3_get_interpolant in the C/C++ API, which is + * well documented. + * @throws Z3Exception + **/ + Expr[] GetInterpolant(Expr pf, Expr pat, Params p) throws Z3Exception + { + checkContextMatch(pf); + checkContextMatch(pat); + checkContextMatch(p); + + ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject())); + int n = seq.size(); + Expr[] res = new Expr[n]; + for (int i = 0; i < n; i++) + res[i] = Expr.create(this, seq.get(i).getNativeObject()); + return res; + } + + /** + * 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. + * @throws Z3Exception + **/ + Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model) throws Z3Exception + { + checkContextMatch(pat); + checkContextMatch(p); + + Native.LongPtr n_i = new Native.LongPtr(); + Native.LongPtr n_m = new Native.LongPtr(); + int r = Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m); + interp = new ASTVector(this, n_i.value); + model = new Model(this, n_m.value); + return Z3_lbool.fromInt(r); + } + + /// + /// Return a string summarizing cumulative time used for interpolation. + /// + /// For more information on interpolation please refer + /// too the function Z3_interpolation_profile in the C/C++ API, which is + /// well documented. + public String InterpolationProfile() throws Z3Exception + { + return Native.interpolationProfile(nCtx()); + } + + /// + /// Checks the correctness of an interpolant. + /// + /// For more information on interpolation please refer + /// too the function Z3_check_interpolant in the C/C++ API, which is + /// well documented. + public int CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory) throws Z3Exception + { + Native.StringPtr n_err_str = new Native.StringPtr(); + int r = Native.checkInterpolant(nCtx(), + cnsts.length, + Expr.arrayToNative(cnsts), + parents, + Expr.arrayToNative(interps), + n_err_str, + theory.length, + Expr.arrayToNative(theory)); + error = n_err_str.value; + return r; + } + + /// + /// Reads an interpolation problem from a file. + /// + /// 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, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception + { + Native.IntPtr n_num = new Native.IntPtr(); + Native.IntPtr n_num_theory = new Native.IntPtr(); + Native.ObjArrayPtr n_cnsts = new Native.ObjArrayPtr(); + Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr(); + Native.ObjArrayPtr n_theory = new Native.ObjArrayPtr(); + Native.StringPtr n_err_str = new Native.StringPtr(); + int r = Native.readInterpolationProblem(nCtx(), n_num, n_cnsts, n_parents, filename, n_err_str, n_num_theory, n_theory); + int num = n_num.value; + int num_theory = n_num_theory.value; + error = n_err_str.value; + cnsts = new Expr[num]; + parents = new int[num]; + theory = new Expr[num_theory]; + for (int i = 0; i < num; i++) + { + cnsts[i] = Expr.create(this, n_cnsts.value[i]); + parents[i] = n_parents.value[i]; + } + for (int i = 0; i < num_theory; i++) + theory[i] = Expr.create(this, n_theory.value[i]); + return r; + } + + /// + /// Writes an interpolation problem to a file. + /// + /// 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) throws Z3Exception + { + Native.writeInterpolationProblem(nCtx(), cnsts.length, Expr.arrayToNative(cnsts), parents, filename, 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..729851988 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_managed_array(1, AST), _out_managed_array(1, UINT), _in(STRING), _out(STRING), _out(UINT), _out_managed_array(6, 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 }; diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 27014bca9..75d56928e 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -500,7 +500,7 @@ static tactic * mk_using_params(cmd_context & ctx, sexpr * n) { symbol param_name = symbol(norm_param_name(c->get_symbol()).c_str()); c = n->get_child(i); i++; - switch (descrs.get_kind(param_name)) { + switch (descrs.get_kind_in_module(param_name)) { case CPK_INVALID: throw cmd_exception("invalid using-params combinator, unknown parameter ", param_name, c->get_line(), c->get_pos()); case CPK_BOOL: diff --git a/src/util/params.cpp b/src/util/params.cpp index cbb2b2acc..b869f8e3d 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -97,6 +97,35 @@ struct param_descrs::imp { return CPK_INVALID; } + bool split_name(symbol const& name, symbol & prefix, symbol & suffix) const { + if (name.is_numerical()) return false; + char const* str = name.bare_str(); + char const* period = strchr(str,'.'); + if (!period) return false; + svector prefix_((unsigned)(period-str), str); + prefix_.push_back(0); + prefix = symbol(prefix_.c_ptr()); + suffix = symbol(period + 1); + return true; + } + + param_kind get_kind_in_module(symbol & name) const { + param_kind k = get_kind(name); + symbol prefix, suffix; + if (k == CPK_INVALID && split_name(name, prefix, suffix)) { + k = get_kind(suffix); + if (k != CPK_INVALID) { + if (symbol(get_module(suffix)) == prefix) { + name = suffix; + } + else { + k = CPK_INVALID; + } + } + } + return k; + } + char const* get_module(symbol const& name) const { info i; if (m_info.find(name, i)) @@ -230,6 +259,10 @@ void param_descrs::erase(char const * name) { erase(symbol(name)); } +param_kind param_descrs::get_kind_in_module(symbol & name) const { + return m_imp->get_kind_in_module(name); +} + param_kind param_descrs::get_kind(symbol const & name) const { return m_imp->get_kind(name); } @@ -311,35 +344,13 @@ public: void reset(symbol const & k); void reset(char const * k); - bool split_name(symbol const& name, symbol & prefix, symbol & suffix) { - if (name.is_numerical()) return false; - char const* str = name.bare_str(); - char const* period = strchr(str,'.'); - if (!period) return false; - svector prefix_((unsigned)(period-str), str); - prefix_.push_back(0); - prefix = symbol(prefix_.c_ptr()); - suffix = symbol(period + 1); - return true; - } void validate(param_descrs const & p) { svector::iterator it = m_entries.begin(); svector::iterator end = m_entries.end(); symbol suffix, prefix; for (; it != end; ++it) { - param_kind expected = p.get_kind(it->first); - if (expected == CPK_INVALID && split_name(it->first, prefix, suffix)) { - expected = p.get_kind(suffix); - if (expected != CPK_INVALID) { - if (symbol(p.get_module(suffix)) == prefix) { - it->first = suffix; - } - else { - expected = CPK_INVALID; - } - } - } + param_kind expected = p.get_kind_in_module(it->first); if (expected == CPK_INVALID) { std::stringstream strm; strm << "unknown parameter '" << it->first.str() << "'\n"; diff --git a/src/util/params.h b/src/util/params.h index f11374775..e4a2b3693 100644 --- a/src/util/params.h +++ b/src/util/params.h @@ -123,6 +123,7 @@ public: void erase(symbol const & name); param_kind get_kind(char const * name) const; param_kind get_kind(symbol const & name) const; + param_kind get_kind_in_module(symbol & name) const; char const * get_descr(char const * name) const; char const * get_descr(symbol const & name) const; char const * get_default(char const * name) const;